Proofgold Address

Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition If_Vo3 := λ x0 : ο . λ x1 x2 : ((ι → ο) → ο) → ο . λ x3 : (ι → ο) → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Known prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem If_Vo3_1 : ∀ x0 : ο . ∀ x1 x2 : ((ι → ο) → ο) → ο . x0 ⟶ If_Vo3 x0 x1 x2 = x1 (proof)
Known andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem If_Vo3_0 : ∀ x0 : ο . ∀ x1 x2 : ((ι → ο) → ο) → ο . not x0 ⟶ If_Vo3 x0 x1 x2 = x2 (proof)
Definition Descr_Vo3 := λ x0 : (((ι → ο) → ο) → ο) → ο . λ x1 : (ι → ο) → ο . ∀ x2 : ((ι → ο) → ο) → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo3_prop : ∀ x0 : (((ι → ο) → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : ((ι → ο) → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ((ι → ο) → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo3 x0) (proof)
Definition 1d01c.. := λ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . λ x1 . λ x2 : ((ι → ο) → ο) → ο . ∀ x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → ((ι → ο) → ο) → ο . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo3 := λ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . λ x1 . Descr_Vo3 (1d01c.. x0 x1)
Theorem 17f7b.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : ι → ((ι → ο) → ο) → ο . (∀ x3 . prim1 x3 x1 ⟶ 1d01c.. x0 x3 (x2 x3)) ⟶ 1d01c.. x0 x1 (x0 x1 x2) (proof)
Theorem 7878a.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : ((ι → ο) → ο) → ο . 1d01c.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ((ι → ο) → ο) → ο . and (∀ x5 . prim1 x5 x1 ⟶ 1d01c.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Known In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem 57733.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ((ι → ο) → ο) → ο . 1d01c.. x0 x1 x2 ⟶ 1d01c.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem fe0b2.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 1d01c.. x0 x1 (In_rec_Vo3 x0 x1) (proof)
Theorem 5fe7e.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 1d01c.. x0 x1 (x0 x1 (In_rec_Vo3 x0)) (proof)
Theorem In_rec_Vo3_eq : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_Vo3 x0 x1 = x0 x1 (In_rec_Vo3 x0) (proof)
Definition bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition inv := λ x0 . λ x1 : ι → ι . λ x2 . prim0 (λ x3 . and (prim1 x3 x0) (x1 x3 = x2))
Known Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Theorem surj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ ∀ x3 . prim1 x3 x1 ⟶ and (prim1 (inv x0 x2 x3) x0) (x2 (inv x0 x2 x3) = x3) (proof)
Theorem f775d.. : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ ∀ x3 . prim1 x3 x0 ⟶ inv x0 x2 (x2 x3) = x3 (proof)
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem bij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ bij x1 x0 (inv x0 x2) (proof)
Theorem bij_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . bij x0 x1 x3 ⟶ bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5)) (proof)
Theorem bij_id : ∀ x0 . bij x0 x0 (λ x1 . x1) (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition exactly1of2 := λ x0 x1 : ο . or (and x0 (not x1)) (and (not x0) x1)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem exactly1of2_I1 : ∀ x0 x1 : ο . x0 ⟶ not x1 ⟶ exactly1of2 x0 x1 (proof)
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem exactly1of2_I2 : ∀ x0 x1 : ο . not x0 ⟶ x1 ⟶ exactly1of2 x0 x1 (proof)
Known xm : ∀ x0 : ο . or x0 (not x0)
Theorem exactly1of2_impI1 : ∀ x0 x1 : ο . (x0 ⟶ not x1) ⟶ (not x0 ⟶ x1) ⟶ exactly1of2 x0 x1 (proof)
Theorem exactly1of2_impI2 : ∀ x0 x1 : ο . (x1 ⟶ not x0) ⟶ (not x1 ⟶ x0) ⟶ exactly1of2 x0 x1 (proof)
Theorem exactly1of2_E : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ not x1 ⟶ x2) ⟶ (not x0 ⟶ x1 ⟶ x2) ⟶ x2 (proof)
Theorem exactly1of2_or : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ or x0 x1 (proof)
Theorem exactly1of2_impn12 : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ x0 ⟶ not x1 (proof)
Theorem exactly1of2_impn21 : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ x1 ⟶ not x0 (proof)
Theorem exactly1of2_nimp12 : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ not x0 ⟶ x1 (proof)
Theorem exactly1of2_nimp21 : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ not x1 ⟶ x0 (proof)
Definition exactly1of3 := λ x0 x1 x2 : ο . or (and (exactly1of2 x0 x1) (not x2)) (and (and (not x0) (not x1)) x2)
Theorem exactly1of3_I1 : ∀ x0 x1 x2 : ο . x0 ⟶ not x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_I2 : ∀ x0 x1 x2 : ο . not x0 ⟶ x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_I3 : ∀ x0 x1 x2 : ο . not x0 ⟶ not x1 ⟶ x2 ⟶ exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_impI1 : ∀ x0 x1 x2 : ο . (x0 ⟶ not x1) ⟶ (x0 ⟶ not x2) ⟶ (x1 ⟶ not x2) ⟶ (not x0 ⟶ or x1 x2) ⟶ exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_impI2 : ∀ x0 x1 x2 : ο . (x1 ⟶ not x0) ⟶ (x1 ⟶ not x2) ⟶ (x0 ⟶ not x2) ⟶ (not x1 ⟶ or x0 x2) ⟶ exactly1of3 x0 x1 x2 (proof)
Theorem exactly1of3_impI3 : ∀ x0 x1 x2 : ο . (x2 ⟶ not x0) ⟶ (x2 ⟶ not x1) ⟶ (x0 ⟶ not x1) ⟶ (not x0 ⟶ x1) ⟶ exactly1of3 x0 x1 x2 (proof)
Known and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem exactly1of3_E : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ ∀ x3 : ο . (x0 ⟶ not x1 ⟶ not x2 ⟶ x3) ⟶ (not x0 ⟶ x1 ⟶ not x2 ⟶ x3) ⟶ (not x0 ⟶ not x1 ⟶ x2 ⟶ x3) ⟶ x3 (proof)
Known or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Known or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Known or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Theorem exactly1of3_or : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ or (or x0 x1) x2 (proof)
Theorem exactly1of3_impn12 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x0 ⟶ not x1 (proof)
Theorem exactly1of3_impn13 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x0 ⟶ not x2 (proof)
Theorem exactly1of3_impn21 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x1 ⟶ not x0 (proof)
Theorem exactly1of3_impn23 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x1 ⟶ not x2 (proof)
Theorem exactly1of3_impn31 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x2 ⟶ not x0 (proof)
Theorem exactly1of3_impn32 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x2 ⟶ not x1 (proof)
Theorem exactly1of3_nimp1 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ not x0 ⟶ or x1 x2 (proof)
Theorem exactly1of3_nimp2 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ not x1 ⟶ or x0 x2 (proof)
Theorem exactly1of3_nimp3 : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ not x2 ⟶ or x0 x1 (proof)
Definition Descr_Vo1 := λ x0 : (ι → ο) → ο . λ x1 . ∀ x2 : ι → ο . x0 x2 ⟶ x2 x1
Definition reflexive := λ x0 : ι → ι → ο . ∀ x1 . x0 x1 x1
Definition irreflexive := λ x0 : ι → ι → ο . ∀ x1 . not (x0 x1 x1)
Definition symmetric := λ x0 : ι → ι → ο . ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1
Definition antisymmetric := λ x0 : ι → ι → ο . ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1 ⟶ x1 = x2
Definition transitive := λ x0 : ι → ι → ο . ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x2 x3 ⟶ x0 x1 x3
Definition eqreln := λ x0 : ι → ι → ο . and (and (reflexive x0) (symmetric x0)) (transitive x0)
Definition per := λ x0 : ι → ι → ο . and (symmetric x0) (transitive x0)
Definition linear := λ x0 : ι → ι → ο . ∀ x1 x2 . or (x0 x1 x2) (x0 x2 x1)
Definition trichotomous_or := λ x0 : ι → ι → ο . ∀ x1 x2 . or (or (x0 x1 x2) (x1 = x2)) (x0 x2 x1)
Definition partialorder := λ x0 : ι → ι → ο . and (and (reflexive x0) (antisymmetric x0)) (transitive x0)
Definition totalorder := λ x0 : ι → ι → ο . and (partialorder x0) (linear x0)
Definition strictpartialorder := λ x0 : ι → ι → ο . and (irreflexive x0) (transitive x0)
Definition stricttotalorder := λ x0 : ι → ι → ο . and (strictpartialorder x0) (trichotomous_or x0)
Theorem per_sym : ∀ x0 : ι → ι → ο . per x0 ⟶ symmetric x0 (proof)
Theorem per_tra : ∀ x0 : ι → ι → ο . per x0 ⟶ transitive x0 (proof)
Theorem per_stra1 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 x3 . x0 x2 x1 ⟶ x0 x2 x3 ⟶ x0 x1 x3 (proof)
Theorem per_stra2 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x3 x2 ⟶ x0 x1 x3 (proof)
Theorem per_stra3 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 x3 . x0 x2 x1 ⟶ x0 x3 x2 ⟶ x0 x1 x3 (proof)
Theorem per_ref1 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ x0 x1 x1 (proof)
Theorem per_ref2 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x2 (proof)
Theorem partialorder_strictpartialorder : ∀ x0 : ι → ι → ο . partialorder x0 ⟶ strictpartialorder (λ x1 x2 . and (x0 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)) (proof)
Definition reflclos := λ x0 : ι → ι → ο . λ x1 x2 . or (x0 x1 x2) (x1 = x2)
Theorem reflclos_refl : ∀ x0 : ι → ι → ο . reflexive (reflclos x0) (proof)
Theorem reflclos_min : ∀ x0 x1 : ι → ι → ο . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3) ⟶ reflexive x1 ⟶ ∀ x2 x3 . reflclos x0 x2 x3 ⟶ x1 x2 x3 (proof)
Theorem strictpartialorder_partialorder_reflclos : ∀ x0 : ι → ι → ο . strictpartialorder x0 ⟶ partialorder (reflclos x0) (proof)
Known or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Theorem stricttotalorder_totalorder_reflclos : ∀ x0 : ι → ι → ο . stricttotalorder x0 ⟶ totalorder (reflclos x0) (proof)
Theorem 64052.. : ∀ x0 : ι → ο . (∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ x1 (λ x3 . and (x2 x3) (x3 = prim0 x2 ⟶ ∀ x4 : ο . x4))) ⟶ (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2)) ⟶ x1 x0) ⟶ ∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ x1 (λ x3 . and (x2 x3) (x3 = prim0 x2 ⟶ ∀ x4 : ο . x4))) ⟶ (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2)) ⟶ x1 (λ x2 . and (x0 x2) (x2 = prim0 x0 ⟶ ∀ x3 : ο . x3)) (proof)
Theorem 0fb6a.. : ∀ x0 : (ι → ο) → ο . (∀ x1 : ι → ο . x0 x1 ⟶ ∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x2 (λ x4 . and (x3 x4) (x4 = prim0 x3 ⟶ ∀ x5 : ο . x5))) ⟶ (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x2 x4) ⟶ x2 (Descr_Vo1 x3)) ⟶ x2 x1) ⟶ ∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ x1 (λ x3 . and (x2 x3) (x3 = prim0 x2 ⟶ ∀ x4 : ο . x4))) ⟶ (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2)) ⟶ x1 (Descr_Vo1 x0) (proof)
Theorem c6cad.. : ∀ x0 : (ι → ο) → ο . (∀ x1 : ι → ο . (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x2 (λ x4 . and (x3 x4) (x4 = prim0 x3 ⟶ ∀ x5 : ο . x5))) ⟶ (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x2 x4) ⟶ x2 (Descr_Vo1 x3)) ⟶ x2 x1) ⟶ x0 x1 ⟶ x0 (λ x2 . and (x1 x2) (x2 = prim0 x1 ⟶ ∀ x3 : ο . x3))) ⟶ (∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ ∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x3 (λ x5 . and (x4 x5) (x5 = prim0 x4 ⟶ ∀ x6 : ο . x6))) ⟶ (∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . x4 x5 ⟶ x3 x5) ⟶ x3 (Descr_Vo1 x4)) ⟶ x3 x2) ⟶ (∀ x2 : ι → ο . x1 x2 ⟶ x0 x2) ⟶ x0 (Descr_Vo1 x1)) ⟶ ∀ x1 : ι → ο . (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x2 (λ x4 . and (x3 x4) (x4 = prim0 x3 ⟶ ∀ x5 : ο . x5))) ⟶ (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x2 x4) ⟶ x2 (Descr_Vo1 x3)) ⟶ x2 x1) ⟶ x0 x1 (proof)
Known pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Theorem 174d6.. : ∀ x0 : ι → ο . (∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ x1 (λ x3 . and (x2 x3) (x3 = prim0 x2 ⟶ ∀ x4 : ο . x4))) ⟶ (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2)) ⟶ x1 x0) ⟶ ∀ x1 : ι → ο . (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x2 (λ x4 . and (x3 x4) (x4 = prim0 x3 ⟶ ∀ x5 : ο . x5))) ⟶ (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x2 x4) ⟶ x2 (Descr_Vo1 x3)) ⟶ x2 x1) ⟶ or (∀ x2 . x1 x2 ⟶ x0 x2) (∀ x2 . x0 x2 ⟶ x1 x2) (proof)
Theorem f5a39.. : ∀ x0 : ι → ο . (∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ x1 (λ x3 . and (x2 x3) (x3 = prim0 x2 ⟶ ∀ x4 : ο . x4))) ⟶ (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2)) ⟶ x1 x0) ⟶ ∀ x1 : ι → ο . (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x2 (λ x4 . and (x3 x4) (x4 = prim0 x3 ⟶ ∀ x5 : ο . x5))) ⟶ (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x2 x4) ⟶ x2 (Descr_Vo1 x3)) ⟶ x2 x1) ⟶ x1 (prim0 x0) ⟶ ∀ x2 . x0 x2 ⟶ x1 x2 (proof)
Theorem c81f6.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ x1 (λ x3 . and (x2 x3) (x3 = prim0 x2 ⟶ ∀ x4 : ο . x4))) ⟶ (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2)) ⟶ x1 (Descr_Vo1 (λ x2 : ι → ο . and (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x3 (λ x5 . and (x4 x5) (x5 = prim0 x4 ⟶ ∀ x6 : ο . x6))) ⟶ (∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . x4 x5 ⟶ x3 x5) ⟶ x3 (Descr_Vo1 x4)) ⟶ x3 x2) (∀ x3 . x0 x3 ⟶ x2 x3))) (proof)
Theorem 5d753.. : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ Descr_Vo1 (λ x2 : ι → ο . and (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x3 (λ x5 . and (x4 x5) (x5 = prim0 x4 ⟶ ∀ x6 : ο . x6))) ⟶ (∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . x4 x5 ⟶ x3 x5) ⟶ x3 (Descr_Vo1 x4)) ⟶ x3 x2) (∀ x3 . x0 x3 ⟶ x2 x3)) x1 (proof)
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem c7682.. : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 (Descr_Vo1 (λ x1 : ι → ο . and (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x2 (λ x4 . and (x3 x4) (x4 = prim0 x3 ⟶ ∀ x5 : ο . x5))) ⟶ (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x2 x4) ⟶ x2 (Descr_Vo1 x3)) ⟶ x2 x1) (∀ x2 . x0 x2 ⟶ x1 x2)))) (proof)
Definition ZermeloWO := λ x0 . Descr_Vo1 (λ x1 : ι → ο . and (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x2 (λ x4 . and (x3 x4) (x4 = prim0 x3 ⟶ ∀ x5 : ο . x5))) ⟶ (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x2 x4) ⟶ x2 (Descr_Vo1 x3)) ⟶ x2 x1) (∀ x2 . x2 = x0 ⟶ x1 x2))
Theorem a68ca.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ x1 (λ x3 . and (x2 x3) (x3 = prim0 x2 ⟶ ∀ x4 : ο . x4))) ⟶ (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2)) ⟶ x1 (ZermeloWO x0) (proof)
Theorem ZermeloWO_ref : reflexive ZermeloWO (proof)
Theorem ZermeloWO_Eps : ∀ x0 . prim0 (ZermeloWO x0) = x0 (proof)
Theorem ZermeloWO_lin : linear ZermeloWO (proof)
Theorem ZermeloWO_tra : transitive ZermeloWO (proof)
Theorem ZermeloWO_antisym : antisymmetric ZermeloWO (proof)
Theorem ZermeloWO_partialorder : partialorder ZermeloWO (proof)
Theorem ZermeloWO_totalorder : totalorder ZermeloWO (proof)
Theorem ZermeloWO_wo : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ ∀ x1 : ο . (∀ x2 . and (x0 x2) (∀ x3 . x0 x3 ⟶ ZermeloWO x2 x3) ⟶ x1) ⟶ x1 (proof)
Definition ZermeloWOstrict := λ x0 x1 . and (ZermeloWO x0 x1) (x0 = x1 ⟶ ∀ x2 : ο . x2)
Theorem ZermeloWOstrict_trich : trichotomous_or ZermeloWOstrict (proof)
Theorem ZermeloWOstrict_stricttotalorder : stricttotalorder ZermeloWOstrict (proof)
Theorem ZermeloWOstrict_wo : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ ∀ x1 : ο . (∀ x2 . and (x0 x2) (∀ x3 . and (x0 x3) (x3 = x2 ⟶ ∀ x4 : ο . x4) ⟶ ZermeloWOstrict x2 x3) ⟶ x1) ⟶ x1 (proof)
Theorem Zermelo_WO : ∀ x0 : ο . (∀ x1 : ι → ι → ο . and (totalorder x1) (∀ x2 : ι → ο . (∀ x3 : ο . (∀ x4 . x2 x4 ⟶ x3) ⟶ x3) ⟶ ∀ x3 : ο . (∀ x4 . and (x2 x4) (∀ x5 . x2 x5 ⟶ x1 x4 x5) ⟶ x3) ⟶ x3) ⟶ x0) ⟶ x0 (proof)
Theorem Zermelo_WO_strict : ∀ x0 : ο . (∀ x1 : ι → ι → ο . and (stricttotalorder x1) (∀ x2 : ι → ο . (∀ x3 : ο . (∀ x4 . x2 x4 ⟶ x3) ⟶ x3) ⟶ ∀ x3 : ο . (∀ x4 . and (x2 x4) (∀ x5 . and (x2 x5) (x5 = x4 ⟶ ∀ x6 : ο . x6) ⟶ x1 x4 x5) ⟶ x3) ⟶ x3) ⟶ x0) ⟶ x0 (proof)