Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition If_Vo3^If_Vo3 := λ x0 : ο . λ x1 x2 : ((ι → ο) → ο) → ο . λ x3 : (ι → ο) → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known andEL^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem If_Vo3_1^If_Vo3_1 : ∀ x0 : ο . ∀ x1 x2 : ((ι → ο) → ο) → ο . x0 ⟶ If_Vo3 x0 x1 x2 = x1 (proof)
Known andER^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem If_Vo3_0^If_Vo3_0 : ∀ x0 : ο . ∀ x1 x2 : ((ι → ο) → ο) → ο . not x0 ⟶ If_Vo3 x0 x1 x2 = x2 (proof)
Definition Descr_Vo3^Descr_Vo3 := λ x0 : (((ι → ο) → ο) → ο) → ο . λ x1 : (ι → ο) → ο . ∀ x2 : ((ι → ο) → ο) → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo3_prop^{Descr_Vo3_prop} : ∀ x0 : (((ι → ο) → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : ((ι → ο) → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ((ι → ο) → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo3 x0) (proof)
Definition b9fc2.. := λ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . λ x1 . λ x2 : ((ι → ο) → ο) → ο . ∀ x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → ((ι → ο) → ο) → ο . (∀ x6 . x6 ∈ x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo3^In_rec_Vo3 := λ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . λ x1 . Descr_Vo3 (b9fc2.. x0 x1)
Theorem f621a.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : ι → ((ι → ο) → ο) → ο . (∀ x3 . x3 ∈ x1 ⟶ b9fc2.. x0 x3 (x2 x3)) ⟶ b9fc2.. x0 x1 (x0 x1 x2) (proof)
Theorem 0f3d9.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : ((ι → ο) → ο) → ο . b9fc2.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ((ι → ο) → ο) → ο . and (∀ x5 . x5 ∈ x1 ⟶ b9fc2.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Known In_ind^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem 387ad.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ((ι → ο) → ο) → ο . b9fc2.. x0 x1 x2 ⟶ b9fc2.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem e24c6.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . b9fc2.. x0 x1 (In_rec_Vo3 x0 x1) (proof)
Theorem 495f3.. : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . b9fc2.. x0 x1 (x0 x1 (In_rec_Vo3 x0)) (proof)
Theorem In_rec_Vo3_eq^{In_rec_Vo3_eq} : ∀ x0 : ι → (ι → ((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . 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^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition inv^inv := λ x0 . λ x1 : ι → ι . λ x2 . prim0 (λ x3 . and (x3 ∈ x0) (x1 x3 = x2))
Known Eps_i_ax^Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Known surj_rinv^surj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ ∀ x3 . x3 ∈ x1 ⟶ and (inv x0 x2 x3 ∈ x0) (x2 (inv x0 x2 x3) = x3)
Known inj_linv_coddep : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ ∀ x3 . x3 ∈ x0 ⟶ inv x0 x2 (x2 x3) = x3
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known bij_inv^bij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ bij x1 x0 (inv x0 x2)
Known bij_comp^bij_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . bij x0 x1 x3 ⟶ bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5))
Known bij_id^bij_id : ∀ x0 . bij x0 x0 (λ x1 . x1)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition exactly1of2^exactly1of2 := λ x0 x1 : ο . or (and x0 (not x1)) (and (not x0) x1)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known exactly1of2_I1^{exactly1of2_I1} : ∀ x0 x1 : ο . x0 ⟶ not x1 ⟶ exactly1of2 x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known exactly1of2_I2^{exactly1of2_I2} : ∀ x0 x1 : ο . not x0 ⟶ x1 ⟶ exactly1of2 x0 x1
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known exactly1of2_impI1^{exactly1of2_impI1} : ∀ x0 x1 : ο . (x0 ⟶ not x1) ⟶ (not x0 ⟶ x1) ⟶ exactly1of2 x0 x1
Known exactly1of2_impI2^{exactly1of2_impI2} : ∀ x0 x1 : ο . (x1 ⟶ not x0) ⟶ (not x1 ⟶ x0) ⟶ exactly1of2 x0 x1
Known exactly1of2_E^{exactly1of2_E} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ not x1 ⟶ x2) ⟶ (not x0 ⟶ x1 ⟶ x2) ⟶ x2
Known exactly1of2_or^{exactly1of2_or} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ or x0 x1
Known exactly1of2_impn12^{exactly1of2_impn12} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ x0 ⟶ not x1
Known exactly1of2_impn21^{exactly1of2_impn21} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ x1 ⟶ not x0
Known exactly1of2_nimp12^{exactly1of2_nimp12} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ not x0 ⟶ x1
Known exactly1of2_nimp21^{exactly1of2_nimp21} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ not x1 ⟶ x0
Definition exactly1of3^exactly1of3 := λ x0 x1 x2 : ο . or (and (exactly1of2 x0 x1) (not x2)) (and (and (not x0) (not x1)) x2)
Known exactly1of3_I1^{exactly1of3_I1} : ∀ x0 x1 x2 : ο . x0 ⟶ not x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2
Known exactly1of3_I2^{exactly1of3_I2} : ∀ x0 x1 x2 : ο . not x0 ⟶ x1 ⟶ not x2 ⟶ exactly1of3 x0 x1 x2
Known exactly1of3_I3^{exactly1of3_I3} : ∀ x0 x1 x2 : ο . not x0 ⟶ not x1 ⟶ x2 ⟶ exactly1of3 x0 x1 x2
Known exactly1of3_impI1^{exactly1of3_impI1} : ∀ x0 x1 x2 : ο . (x0 ⟶ not x1) ⟶ (x0 ⟶ not x2) ⟶ (x1 ⟶ not x2) ⟶ (not x0 ⟶ or x1 x2) ⟶ exactly1of3 x0 x1 x2
Known exactly1of3_impI2^{exactly1of3_impI2} : ∀ x0 x1 x2 : ο . (x1 ⟶ not x0) ⟶ (x1 ⟶ not x2) ⟶ (x0 ⟶ not x2) ⟶ (not x1 ⟶ or x0 x2) ⟶ exactly1of3 x0 x1 x2
Known exactly1of3_impI3^{exactly1of3_impI3} : ∀ x0 x1 x2 : ο . (x2 ⟶ not x0) ⟶ (x2 ⟶ not x1) ⟶ (x0 ⟶ not x1) ⟶ (not x0 ⟶ x1) ⟶ exactly1of3 x0 x1 x2
Known and3E^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Known exactly1of3_E^{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
Known or3I1^or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Known or3I2^or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Known or3I3^or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Known exactly1of3_or^{exactly1of3_or} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ or (or x0 x1) x2
Known exactly1of3_impn12^{exactly1of3_impn12} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x0 ⟶ not x1
Known exactly1of3_impn13^{exactly1of3_impn13} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x0 ⟶ not x2
Known exactly1of3_impn21^{exactly1of3_impn21} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x1 ⟶ not x0
Known exactly1of3_impn23^{exactly1of3_impn23} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x1 ⟶ not x2
Known exactly1of3_impn31^{exactly1of3_impn31} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x2 ⟶ not x0
Known exactly1of3_impn32^{exactly1of3_impn32} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ x2 ⟶ not x1
Known exactly1of3_nimp1^{exactly1of3_nimp1} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ not x0 ⟶ or x1 x2
Known exactly1of3_nimp2^{exactly1of3_nimp2} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ not x1 ⟶ or x0 x2
Known exactly1of3_nimp3^{exactly1of3_nimp3} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ not x2 ⟶ or x0 x1
Definition Descr_Vo1^Descr_Vo1 := λ x0 : (ι → ο) → ο . λ x1 . ∀ x2 : ι → ο . x0 x2 ⟶ x2 x1
Definition reflexive^reflexive := λ x0 : ι → ι → ο . ∀ x1 . x0 x1 x1
Definition irreflexive^irreflexive := λ x0 : ι → ι → ο . ∀ x1 . not (x0 x1 x1)
Definition symmetric^symmetric := λ x0 : ι → ι → ο . ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1
Definition antisymmetric^{antisymmetric} := λ x0 : ι → ι → ο . ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1 ⟶ x1 = x2
Definition transitive^transitive := λ x0 : ι → ι → ο . ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x2 x3 ⟶ x0 x1 x3
Definition eqreln^eqreln := λ x0 : ι → ι → ο . and (and (reflexive x0) (symmetric x0)) (transitive x0)
Definition per^per := λ x0 : ι → ι → ο . and (symmetric x0) (transitive x0)
Definition linear^linear := λ x0 : ι → ι → ο . ∀ x1 x2 . or (x0 x1 x2) (x0 x2 x1)
Definition trichotomous_or^{trichotomous_or} := λ x0 : ι → ι → ο . ∀ x1 x2 . or (or (x0 x1 x2) (x1 = x2)) (x0 x2 x1)
Definition partialorder^partialorder := λ x0 : ι → ι → ο . and (and (reflexive x0) (antisymmetric x0)) (transitive x0)
Definition totalorder^totalorder := λ x0 : ι → ι → ο . and (partialorder x0) (linear x0)
Definition strictpartialorder^{strictpartialorder} := λ x0 : ι → ι → ο . and (irreflexive x0) (transitive x0)
Definition stricttotalorder^{stricttotalorder} := λ x0 : ι → ι → ο . and (strictpartialorder x0) (trichotomous_or x0)
Theorem per_sym^per_sym : ∀ x0 : ι → ι → ο . per x0 ⟶ symmetric x0 (proof)
Theorem per_tra^per_tra : ∀ x0 : ι → ι → ο . per x0 ⟶ transitive x0 (proof)
Theorem per_stra1^per_stra1 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 x3 . x0 x2 x1 ⟶ x0 x2 x3 ⟶ x0 x1 x3 (proof)
Theorem per_stra2^per_stra2 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x3 x2 ⟶ x0 x1 x3 (proof)
Theorem per_stra3^per_stra3 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 x3 . x0 x2 x1 ⟶ x0 x3 x2 ⟶ x0 x1 x3 (proof)
Theorem per_ref1^per_ref1 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ x0 x1 x1 (proof)
Theorem per_ref2^per_ref2 : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x2 (proof)
Theorem partialorder_strictpartialorder^{partialorder_strictpartialorder} : ∀ x0 : ι → ι → ο . partialorder x0 ⟶ strictpartialorder (λ x1 x2 . and (x0 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)) (proof)
Definition reflclos^reflclos := λ x0 : ι → ι → ο . λ x1 x2 . or (x0 x1 x2) (x1 = x2)
Theorem reflclos_refl^{reflclos_refl} : ∀ x0 : ι → ι → ο . reflexive (reflclos x0) (proof)
Theorem reflclos_min^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^{strictpartialorder_partialorder_reflclos} : ∀ x0 : ι → ι → ο . strictpartialorder x0 ⟶ partialorder (reflclos x0) (proof)
Known or3E^or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Theorem stricttotalorder_totalorder_reflclos^{stricttotalorder_totalorder_reflclos} : ∀ x0 : ι → ι → ο . stricttotalorder x0 ⟶ totalorder (reflclos x0) (proof)
Theorem 9e56d.. : ∀ 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 588d8.. : ∀ 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 ef1ce.. : ∀ 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^pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Theorem 484e2.. : ∀ 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 60d40.. : ∀ 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 d31dd.. : ∀ 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 d2f26.. : ∀ 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^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem d5dd5.. : ∀ 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^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 b9994.. : ∀ 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^{ZermeloWO_ref} : reflexive ZermeloWO (proof)
Theorem ZermeloWO_Eps^{ZermeloWO_Eps} : ∀ x0 . prim0 (ZermeloWO x0) = x0 (proof)
Theorem ZermeloWO_lin^{ZermeloWO_lin} : linear ZermeloWO (proof)
Theorem ZermeloWO_tra^{ZermeloWO_tra} : transitive ZermeloWO (proof)
Theorem ZermeloWO_antisym^{ZermeloWO_antisym} : antisymmetric ZermeloWO (proof)
Theorem ZermeloWO_partialorder^{ZermeloWO_partialorder} : partialorder ZermeloWO (proof)
Theorem ZermeloWO_totalorder^{ZermeloWO_totalorder} : totalorder ZermeloWO (proof)
Theorem ZermeloWO_wo^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^{ZermeloWOstrict} := λ x0 x1 . and (ZermeloWO x0 x1) (x0 = x1 ⟶ ∀ x2 : ο . x2)
Theorem ZermeloWOstrict_trich^{ZermeloWOstrict_trich} : trichotomous_or ZermeloWOstrict (proof)
Theorem ZermeloWOstrict_stricttotalorder^{ZermeloWOstrict_stricttotalorder} : stricttotalorder ZermeloWOstrict (proof)
Theorem ZermeloWOstrict_wo^{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^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^{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)