Nuprl Lemma : set-axiom-of-choice-implies-xmiddle

Set-AC  (∀P:ℙ((↓P) ∨ P)))


Proof




Definitions occuring in Statement :  set-axiom-of-choice: Set-AC prop: all: x:A. B[x] not: ¬A squash: T implies:  Q or: P ∨ Q
Definitions unfolded in proof :  implies:  Q all: x:A. B[x] set-axiom-of-choice: Set-AC member: t ∈ T uall: [x:A]. B[x] int_seg: {i..j-} or: P ∨ Q prop: bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) not: ¬A less_than: a < b squash: T true: True nequal: a ≠ b ∈  subtype_rel: A ⊆B decidable: Dec(P) top: Top eq_int: (i =z j) ext-eq: A ≡ B so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  int_seg_wf ifthenelse_wf eq_int_wf or_wf equal-wf-T-base set-axiom-of-choice_wf bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int false_wf lelt_wf decidable__equal_int_seg le_antisymmetry_iff add_functionality_wrt_le add-associates add-swap add-commutes add-zero le-add-cancel not_wf squash_wf subtype_rel_sets
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution cut hypothesis dependent_functionElimination thin introduction extract_by_obid isectElimination natural_numberEquality lambdaEquality instantiate setElimination rename hypothesisEquality universeEquality setEquality intEquality baseClosed because_Cache independent_functionElimination sqequalRule unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination dependent_pairFormation promote_hyp cumulativity voidElimination dependent_set_memberEquality independent_pairFormation imageMemberEquality inlFormation applyEquality functionExtensionality applyLambdaEquality imageElimination addEquality isect_memberEquality voidEquality inrFormation

Latex:
Set-AC  {}\mRightarrow{}  (\mforall{}P:\mBbbP{}.  ((\mdownarrow{}P)  \mvee{}  (\mneg{}P)))



Date html generated: 2017_04_14-AM-07_37_44
Last ObjectModification: 2017_02_27-PM-03_10_05

Theory : subtype_1


Home Index