Proofgold Address

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Param 91630.. : ι → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Known c8c18.. : 4a7ef.. = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Theorem 76294.. : not (TransSet (91630.. (4ae4a.. 4a7ef..))) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Theorem c2694.. : not (ordinal (91630.. (4ae4a.. 4a7ef..))) (proof)
Param 0ac37.. : ι → ι → ι
Definition 15418.. := λ x0 x1 . 0ac37.. x0 (91630.. x1)
Known ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1
Known 287ca.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 x2 (0ac37.. x0 x1)
Theorem e9d4c.. : ∀ x0 . not (ordinal (15418.. x0 (91630.. (4ae4a.. 4a7ef..)))) (proof)
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Theorem 04665.. : ∀ x0 x1 . ordinal x0 ⟶ nIn (15418.. x1 (91630.. (4ae4a.. 4a7ef..))) x0 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known edd11.. : ∀ x0 x1 x2 . prim1 x2 (0ac37.. x0 x1) ⟶ or (prim1 x2 x0) (prim1 x2 x1)
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known da962.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 (0ac37.. x0 x1)
Theorem fb3f3.. : ∀ x0 x1 . ordinal x0 ⟶ 15418.. x0 (91630.. (4ae4a.. 4a7ef..)) = 15418.. x1 (91630.. (4ae4a.. 4a7ef..)) ⟶ Subq x0 x1 (proof)
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem a4673.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ 15418.. x0 (91630.. (4ae4a.. 4a7ef..)) = 15418.. x1 (91630.. (4ae4a.. 4a7ef..)) ⟶ x0 = x1 (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem 48c17.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ prim1 (15418.. x1 (91630.. (4ae4a.. 4a7ef..))) (94f9e.. x0 (λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..)))) ⟶ prim1 x1 x0 (proof)
Theorem 332b1.. : ∀ x0 x1 . ordinal x0 ⟶ nIn x0 (94f9e.. x1 (λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..)))) (proof)
Definition 472ec.. := λ x0 . 0ac37.. x0 (94f9e.. x0 (λ x1 . 15418.. x1 (91630.. (4ae4a.. 4a7ef..))))
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem e52f8.. : ∀ x0 x1 . Subq x0 x1 ⟶ Subq (472ec.. x0) (472ec.. x1) (proof)
Param exactly1of2 : ο → ο → ο
Definition 1beb9.. := λ x0 x1 . and (Subq x1 (472ec.. x0)) (∀ x2 . prim1 x2 x0 ⟶ exactly1of2 (prim1 (15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1) (prim1 x2 x1))
Param 1216a.. : ι → (ι → ο) → ι
Param a4c2a.. : ι → (ι → ο) → (ι → ι) → ι
Definition 09072.. := λ x0 . λ x1 : ι → ο . 0ac37.. (1216a.. x0 x1) (a4c2a.. x0 (λ x2 . not (x1 x2)) (λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))))
Definition iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Definition PNoEq_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Known ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2
Known 932b3.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 (a4c2a.. x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . prim1 x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Theorem db375.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNoEq_ x0 (λ x2 . prim1 x2 (09072.. x0 x1)) x1 (proof)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 6982e.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ and (prim1 x2 x0) (x1 x2)
Known xm : ∀ x0 : ο . or x0 (not x0)
Known exactly1of2_I2 : ∀ x0 x1 : ο . not x0 ⟶ x1 ⟶ exactly1of2 x0 x1
Known exactly1of2_I1 : ∀ x0 x1 : ο . x0 ⟶ not x1 ⟶ exactly1of2 x0 x1
Known e951d.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 x0 ⟶ x1 x3 ⟶ prim1 (x2 x3) (a4c2a.. x0 x1 x2)
Theorem c0a4f.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . 1beb9.. x0 (09072.. x0 x1) (proof)
Known exactly1of2_E : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ not x1 ⟶ x2) ⟶ (not x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem cdf75.. : ∀ x0 x1 . ordinal x0 ⟶ 1beb9.. x0 x1 ⟶ x1 = 09072.. x0 (λ x3 . prim1 x3 x1) (proof)
Definition 80242.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (ordinal x2) (1beb9.. x2 x0) ⟶ x1) ⟶ x1
Theorem 5258d.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 1beb9.. x0 x1 ⟶ 80242.. x1 (proof)
Definition e4431.. := λ x0 . prim0 (λ x1 . and (ordinal x1) (1beb9.. x1 x0))
Known exactly1of2_or : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ or x0 x1
Theorem 7294e.. : ∀ x0 x1 x2 . ordinal x1 ⟶ ordinal x2 ⟶ 1beb9.. x1 x0 ⟶ 1beb9.. x2 x0 ⟶ Subq x1 x2 (proof)
Theorem 0b81c.. : ∀ x0 x1 x2 . ordinal x1 ⟶ ordinal x2 ⟶ 1beb9.. x1 x0 ⟶ 1beb9.. x2 x0 ⟶ x1 = x2 (proof)
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem d8827.. : ∀ x0 . 80242.. x0 ⟶ and (ordinal (e4431.. x0)) (1beb9.. (e4431.. x0) x0) (proof)
Theorem 4c9ee.. : ∀ x0 . 80242.. x0 ⟶ ordinal (e4431.. x0) (proof)
Theorem b0eab.. : ∀ x0 . 80242.. x0 ⟶ 1beb9.. (e4431.. x0) x0 (proof)
Theorem 028bc.. : ∀ x0 . 80242.. x0 ⟶ x0 = 09072.. (e4431.. x0) (λ x2 . prim1 x2 x0) (proof)
Theorem be8b9.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . e4431.. (09072.. x0 x1) = x0 (proof)
Theorem 40c06.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ Subq (e4431.. x0) (e4431.. x1) ⟶ (∀ x2 . prim1 x2 (e4431.. x0) ⟶ iff (prim1 x2 x0) (prim1 x2 x1)) ⟶ Subq x0 x1 (proof)
Definition SNoEq_ := λ x0 x1 x2 . PNoEq_ x0 (λ x3 . prim1 x3 x1) (λ x3 . prim1 x3 x2)
Theorem SNoEq_I : ∀ x0 x1 x2 . (∀ x3 . prim1 x3 x0 ⟶ iff (prim1 x3 x1) (prim1 x3 x2)) ⟶ SNoEq_ x0 x1 x2 (proof)
Theorem SNoEq_E : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ iff (prim1 x3 x1) (prim1 x3 x2) (proof)
Theorem SNoEq_E1 : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 x3 x1 ⟶ prim1 x3 x2 (proof)
Theorem SNoEq_E2 : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 x3 x2 ⟶ prim1 x3 x1 (proof)
Known PNoEq_antimon_ : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . prim1 x3 x2 ⟶ PNoEq_ x2 x0 x1 ⟶ PNoEq_ x3 x0 x1
Theorem SNoEq_antimon_ : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ∀ x2 x3 . SNoEq_ x0 x2 x3 ⟶ SNoEq_ x1 x2 x3 (proof)
Known Subq_ref : ∀ x0 . Subq x0 x0
Known iff_sym : ∀ x0 x1 : ο . iff x0 x1 ⟶ iff x1 x0
Theorem 2b8be.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ e4431.. x0 = e4431.. x1 ⟶ SNoEq_ (e4431.. x0) x0 x1 ⟶ x0 = x1 (proof)
Param 40dde.. : ι → (ι → ο) → ι → (ι → ο) → ο
Definition 099f3.. := λ x0 x1 . 40dde.. (e4431.. x0) (λ x2 . prim1 x2 x0) (e4431.. x1) (λ x2 . prim1 x2 x1)
Definition 35b9b.. := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (40dde.. x0 x1 x2 x3) (and (x0 = x2) (PNoEq_ x0 x1 x3))
Definition fe4bb.. := λ x0 x1 . 35b9b.. (e4431.. x0) (λ x2 . prim1 x2 x0) (e4431.. x1) (λ x2 . prim1 x2 x1)
Known 8fc51.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 40dde.. x0 x2 x1 x3 ⟶ 35b9b.. x0 x2 x1 x3
Theorem 8dc73.. : ∀ x0 x1 . 099f3.. x0 x1 ⟶ fe4bb.. x0 x1 (proof)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem 817af.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ fe4bb.. x0 x1 ⟶ or (099f3.. x0 x1) (x0 = x1) (proof)
Known PNoEq_ref_ : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 x1
Theorem SNoEq_ref_ : ∀ x0 x1 . SNoEq_ x0 x1 x1 (proof)
Known PNoEq_sym_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x1
Theorem SNoEq_sym_ : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ SNoEq_ x0 x2 x1 (proof)
Known PNoEq_tra_ : ∀ x0 . ∀ x1 x2 x3 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x3 ⟶ PNoEq_ x0 x1 x3
Theorem SNoEq_tra_ : ∀ x0 x1 x2 x3 . SNoEq_ x0 x1 x2 ⟶ SNoEq_ x0 x2 x3 ⟶ SNoEq_ x0 x1 x3 (proof)
Param d3786.. : ι → ι → ι
Definition PNoLt_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (and (and (PNoEq_ x4 x1 x2) (not (x1 x4))) (x2 x4)) ⟶ x3) ⟶ x3
Known 140e3.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 40dde.. x0 x2 x1 x3 ⟶ ∀ x4 : ο . (PNoLt_ (d3786.. x0 x1) x2 x3 ⟶ x4) ⟶ (prim1 x0 x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ x4) ⟶ (prim1 x1 x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ x4) ⟶ x4
Known PNoLt_E_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoLt_ x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ PNoEq_ x4 x1 x2 ⟶ not (x1 x4) ⟶ x2 x4 ⟶ x3) ⟶ x3
Known 3eff2.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ and (prim1 x2 x0) (prim1 x2 x1)
Known 27954.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . prim1 x1 x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ 40dde.. x0 x2 x1 x3
Known 0f47f.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . prim1 x0 x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ 40dde.. x0 x2 x1 x3
Theorem 36ff9.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . 80242.. x3 ⟶ prim1 (e4431.. x3) (d3786.. (e4431.. x0) (e4431.. x1)) ⟶ SNoEq_ (e4431.. x3) x3 x0 ⟶ SNoEq_ (e4431.. x3) x3 x1 ⟶ 099f3.. x0 x3 ⟶ 099f3.. x3 x1 ⟶ nIn (e4431.. x3) x0 ⟶ prim1 (e4431.. x3) x1 ⟶ x2) ⟶ (prim1 (e4431.. x0) (e4431.. x1) ⟶ SNoEq_ (e4431.. x0) x0 x1 ⟶ prim1 (e4431.. x0) x1 ⟶ x2) ⟶ (prim1 (e4431.. x1) (e4431.. x0) ⟶ SNoEq_ (e4431.. x1) x0 x1 ⟶ nIn (e4431.. x1) x0 ⟶ x2) ⟶ x2 (proof)
Theorem 151ed.. : ∀ x0 x1 . prim1 (e4431.. x0) (e4431.. x1) ⟶ SNoEq_ (e4431.. x0) x0 x1 ⟶ prim1 (e4431.. x0) x1 ⟶ 099f3.. x0 x1 (proof)
Theorem 20dcf.. : ∀ x0 x1 . prim1 (e4431.. x1) (e4431.. x0) ⟶ SNoEq_ (e4431.. x1) x0 x1 ⟶ nIn (e4431.. x1) x0 ⟶ 099f3.. x0 x1 (proof)
Known 7de10.. : ∀ x0 . ∀ x1 : ι → ο . not (40dde.. x0 x1 x0 x1)
Theorem c47c0.. : ∀ x0 . not (099f3.. x0 x0) (proof)
Known 6ace3.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0 ⟶ ordinal x1 ⟶ or (or (40dde.. x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3))) (40dde.. x1 x3 x0 x2)
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 41905.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ or (or (099f3.. x0 x1) (x0 = x1)) (099f3.. x1 x0) (proof)
Known 24a9c.. : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . 40dde.. x0 x3 x1 x4 ⟶ 40dde.. x1 x4 x2 x5 ⟶ 40dde.. x0 x3 x2 x5
Theorem c7cc7.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x1 ⟶ 099f3.. x1 x2 ⟶ 099f3.. x0 x2 (proof)
Known fb736.. : ∀ x0 . ∀ x1 : ι → ο . 35b9b.. x0 x1 x0 x1
Theorem 4c8cc.. : ∀ x0 . fe4bb.. x0 x0 (proof)
Known cd912.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 : ι → ο . 35b9b.. x0 x2 x1 x3 ⟶ 35b9b.. x1 x3 x0 x2 ⟶ and (x0 = x1) (PNoEq_ x0 x2 x3)
Theorem 1a766.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ fe4bb.. x0 x1 ⟶ fe4bb.. x1 x0 ⟶ x0 = x1 (proof)
Known 146ff.. : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . 40dde.. x0 x3 x1 x4 ⟶ 35b9b.. x1 x4 x2 x5 ⟶ 40dde.. x0 x3 x2 x5
Theorem c5dec.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x1 ⟶ fe4bb.. x1 x2 ⟶ 099f3.. x0 x2 (proof)
Known 9652d.. : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . 35b9b.. x0 x3 x1 x4 ⟶ 40dde.. x1 x4 x2 x5 ⟶ 40dde.. x0 x3 x2 x5
Theorem 45d06.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ fe4bb.. x0 x1 ⟶ 099f3.. x1 x2 ⟶ 099f3.. x0 x2 (proof)
Known d1711.. : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . 35b9b.. x0 x3 x1 x4 ⟶ 35b9b.. x1 x4 x2 x5 ⟶ 35b9b.. x0 x3 x2 x5
Theorem 9787a.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ fe4bb.. x0 x1 ⟶ fe4bb.. x1 x2 ⟶ fe4bb.. x0 x2 (proof)
Theorem 027ee.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ or (099f3.. x0 x1) (fe4bb.. x1 x0) (proof)
Known 1f4e8.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoEq_ x0 x2 x3 ⟶ 40dde.. x0 x3 x1 x4 ⟶ 40dde.. x0 x2 x1 x4
Known 43fd7.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . 40dde.. x0 x2 x1 x3 ⟶ PNoEq_ x1 x3 x4 ⟶ 40dde.. x0 x2 x1 x4
Theorem 0b036.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0 ⟶ ordinal x1 ⟶ 099f3.. (09072.. x0 x2) (09072.. x1 x3) ⟶ 40dde.. x0 x2 x1 x3 (proof)
Theorem 2f7d9.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0 ⟶ ordinal x1 ⟶ 40dde.. x0 x2 x1 x3 ⟶ 099f3.. (09072.. x0 x2) (09072.. x1 x3) (proof)
Param 7b9f3.. : (ι → (ι → ο) → ο) → (ι → (ι → ο) → ο) → ι
Param ce2d5.. : (ι → (ι → ο) → ο) → (ι → (ι → ο) → ο) → ι → ο
Definition 02a50.. := λ x0 x1 . 09072.. (7b9f3.. (λ x2 . λ x3 : ι → ο . and (ordinal x2) (prim1 (09072.. x2 x3) x0)) (λ x2 . λ x3 : ι → ο . and (ordinal x2) (prim1 (09072.. x2 x3) x1))) (ce2d5.. (λ x2 . λ x3 : ι → ο . and (ordinal x2) (prim1 (09072.. x2 x3) x0)) (λ x2 . λ x3 : ι → ο . and (ordinal x2) (prim1 (09072.. x2 x3) x1)))
Definition 02b90.. := λ x0 x1 . and (and (∀ x2 . prim1 x2 x0 ⟶ 80242.. x2) (∀ x2 . prim1 x2 x1 ⟶ 80242.. x2)) (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3)
Param a842e.. : ι → (ι → ι) → ι
Definition ed32f.. := λ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . x0 x2 x3 ⟶ ∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x1 x4 x5 ⟶ 40dde.. x2 x3 x4 x5
Definition PNo_lenbdd := λ x0 . λ x1 : ι → (ι → ο) → ο . ∀ x2 . ∀ x3 : ι → ο . x1 x2 x3 ⟶ prim1 x2 x0
Definition cae4c.. := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . ordinal x3 ⟶ ∀ x4 : ι → ο . x0 x3 x4 ⟶ 40dde.. x3 x4 x1 x2
Definition bc2b0.. := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . ordinal x3 ⟶ ∀ x4 : ι → ο . x0 x3 x4 ⟶ 40dde.. x1 x2 x3 x4
Definition 47618.. := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (cae4c.. x0 x2 x3) (bc2b0.. x1 x2 x3)
Definition 1a487.. := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (and (ordinal x2) (47618.. x0 x1 x2 x3)) (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 : ι → ο . not (47618.. x0 x1 x4 x5))
Known f06ce.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ 1a487.. x0 x1 (7b9f3.. x0 x1) (ce2d5.. x0 x1)
Known and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Known PNoLt_trichotomy_or_ : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0)
Param 8033b.. : (ι → (ι → ο) → ο) → (ι → (ι → ο) → ο) → ι → (ι → ο) → ο
Definition a59df.. := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (8033b.. x0 x1 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5))) (8033b.. x0 x1 (4ae4a.. x2) (λ x4 . or (x3 x4) (x4 = x2)))
Known 61193.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . a59df.. x0 x1 x2 x3 ⟶ 47618.. x0 x1 x2 x3
Known e4d06.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 x4 : ι → ο . PNoEq_ x2 x3 x4 ⟶ 8033b.. x0 x1 x2 x3 ⟶ 8033b.. x0 x1 x2 x4
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Known iff_trans : ∀ x0 x1 x2 : ο . iff x0 x1 ⟶ iff x1 x2 ⟶ iff x0 x2
Known PNo_extend0_eq : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . and (x1 x2) (x2 = x0 ⟶ ∀ x3 : ο . x3))
Known 45f48.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . prim1 x3 (4ae4a.. x2) ⟶ ∀ x4 : ι → ο . 47618.. x0 x1 x2 x4 ⟶ 8033b.. x0 x1 x3 x4
Known 09068.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) (4ae4a.. x0)
Known PNo_extend1_eq : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . or (x1 x2) (x2 = x0))
Known b72a3.. : ∀ x0 . ordinal x0 ⟶ ordinal (4ae4a.. x0)
Known ordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (prim1 x0 x1) (Subq x1 x0)
Known 00673.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ prim1 (7b9f3.. x0 x1) (4ae4a.. x2)
Known 2236b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 x0 ⟶ prim1 x3 (x1 x2) ⟶ prim1 x3 (a842e.. x0 x1)
Known 5faa3.. : ∀ x0 . prim1 x0 (4ae4a.. x0)
Known ordinal_linear : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (Subq x0 x1) (Subq x1 x0)
Known 02255.. : ∀ x0 x1 . Subq x0 x1 = (0ac37.. x0 x1 = x1)
Known 47e6b.. : ∀ x0 x1 . 0ac37.. x0 x1 = 0ac37.. x1 x0
Known d5fb2.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ordinal (x1 x2)) ⟶ ordinal (a842e.. x0 x1)
Theorem 9b3fd.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ and (and (and (and (80242.. (02a50.. x0 x1)) (prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x2 . 4ae4a.. (e4431.. x2))) (a842e.. x1 (λ x2 . 4ae4a.. (e4431.. x2))))))) (∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1))) (∀ x2 . prim1 x2 x1 ⟶ 099f3.. (02a50.. x0 x1) x2)) (∀ x2 . 80242.. x2 ⟶ (∀ x3 . prim1 x3 x0 ⟶ 099f3.. x3 x2) ⟶ (∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3) ⟶ and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x2)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x2)) (proof)
Param e5b72.. : ι → ι
Definition 56ded.. := λ x0 . 1216a.. (e5b72.. (472ec.. x0)) (λ x1 . ∀ x2 : ο . (∀ x3 . and (prim1 x3 x0) (1beb9.. x3 x1) ⟶ x2) ⟶ x2)
Theorem 1b1bf.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 (56ded.. x0) ⟶ ∀ x2 : ο . (∀ x3 . and (prim1 x3 x0) (1beb9.. x3 x1) ⟶ x2) ⟶ x2 (proof)
Known 3daee.. : ∀ x0 x1 . Subq x1 x0 ⟶ prim1 x1 (e5b72.. x0)
Known Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Theorem ade9f.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 x2 . prim1 x2 x0 ⟶ 1beb9.. x2 x1 ⟶ prim1 x1 (56ded.. x0) (proof)
Theorem b50ea.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ prim1 (e4431.. x0) (e4431.. x1) ⟶ prim1 x0 (56ded.. (e4431.. x1)) (proof)
Theorem d7a3e.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ Subq x0 x1 ⟶ Subq (56ded.. x0) (56ded.. x1) (proof)
Theorem 27bae.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 1beb9.. x0 x1 ⟶ e4431.. x1 = x0 (proof)
Theorem bfaa9.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 (56ded.. x0) ⟶ ∀ x2 : ο . (prim1 (e4431.. x1) x0 ⟶ ordinal (e4431.. x1) ⟶ 80242.. x1 ⟶ 1beb9.. (e4431.. x1) x1 ⟶ x2) ⟶ x2 (proof)
Known In_irref : ∀ x0 . nIn x0 x0
Theorem 1eaea.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (56ded.. (e4431.. x0)) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2 (proof)
Theorem 98928.. : ∀ x0 . 80242.. x0 ⟶ prim1 x0 (56ded.. (4ae4a.. (e4431.. x0))) (proof)
Definition 23e07.. := λ x0 . 1216a.. (56ded.. (e4431.. x0)) (λ x1 . 099f3.. x1 x0)
Definition 5246e.. := λ x0 . 1216a.. (56ded.. (e4431.. x0)) (099f3.. x0)
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known d0a1f.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ prim1 x2 x0
Theorem 23b01.. : ∀ x0 . 80242.. x0 ⟶ 02b90.. (23e07.. x0) (5246e.. x0) (proof)
Theorem cbec9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (23e07.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ x2) ⟶ x2 (proof)
Theorem e76d1.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (5246e.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ x2) ⟶ x2 (proof)
Theorem 63df9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (23e07.. x0) ⟶ prim1 x1 (56ded.. (e4431.. x0)) (proof)
Theorem 54843.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (5246e.. x0) ⟶ prim1 x1 (56ded.. (e4431.. x0)) (proof)
Theorem f5194.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ prim1 x1 (23e07.. x0) (proof)
Theorem 18a76.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ prim1 x1 (5246e.. x0) (proof)
Known ordinal_trichotomy_or : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (prim1 x0 x1) (x0 = x1)) (prim1 x1 x0)
Theorem f6a2d.. : ∀ x0 . 80242.. x0 ⟶ x0 = 02a50.. (23e07.. x0) (5246e.. x0) (proof)
Theorem 5a5d4.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ 80242.. (02a50.. x0 x1) (proof)
Theorem 0888b.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1) (proof)
Theorem 9c8cc.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . prim1 x2 x1 ⟶ 099f3.. (02a50.. x0 x1) x2 (proof)
Theorem c1313.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . 80242.. x2 ⟶ (∀ x3 . prim1 x3 x0 ⟶ 099f3.. x3 x2) ⟶ (∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3) ⟶ and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x2)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x2) (proof)
Known a5fe0.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ prim1 x2 x1
Theorem 6ec49.. : ∀ x0 x1 x2 x3 . 02b90.. x0 x1 ⟶ 02b90.. x2 x3 ⟶ (∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 (02a50.. x2 x3)) ⟶ (∀ x4 . prim1 x4 x3 ⟶ 099f3.. (02a50.. x0 x1) x4) ⟶ fe4bb.. (02a50.. x0 x1) (02a50.. x2 x3) (proof)
Theorem 22361.. : ∀ x0 x1 x2 x3 . 02b90.. x0 x1 ⟶ 02b90.. x2 x3 ⟶ (∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 (02a50.. x2 x3)) ⟶ (∀ x4 . prim1 x4 x1 ⟶ 099f3.. (02a50.. x2 x3) x4) ⟶ (∀ x4 . prim1 x4 x2 ⟶ 099f3.. x4 (02a50.. x0 x1)) ⟶ (∀ x4 . prim1 x4 x3 ⟶ 099f3.. (02a50.. x0 x1) x4) ⟶ 02a50.. x0 x1 = 02a50.. x2 x3 (proof)
Theorem 5b4d8.. : ∀ x0 . ordinal x0 ⟶ 1beb9.. x0 x0 (proof)
Definition 7cb9a.. := λ x0 . 09072.. (4ae4a.. (e4431.. x0)) (λ x1 . and (prim1 x1 x0) (x1 = e4431.. x0 ⟶ ∀ x2 : ο . x2))
Definition 45abd.. := λ x0 . 09072.. (4ae4a.. (e4431.. x0)) (λ x1 . or (prim1 x1 x0) (x1 = e4431.. x0))
Theorem 2228f.. : ∀ x0 . 80242.. x0 ⟶ 1beb9.. (4ae4a.. (e4431.. x0)) (7cb9a.. x0) (proof)
Theorem 22184.. : ∀ x0 . 80242.. x0 ⟶ 1beb9.. (4ae4a.. (e4431.. x0)) (45abd.. x0) (proof)
Theorem ec0f8.. : ∀ x0 . 80242.. x0 ⟶ 80242.. (7cb9a.. x0) (proof)
Theorem 6a87c.. : ∀ x0 . 80242.. x0 ⟶ 80242.. (45abd.. x0) (proof)
Theorem 8e40c.. : ∀ x0 . 80242.. x0 ⟶ e4431.. (7cb9a.. x0) = 4ae4a.. (e4431.. x0) (proof)
Theorem 80851.. : ∀ x0 . 80242.. x0 ⟶ e4431.. (45abd.. x0) = 4ae4a.. (e4431.. x0) (proof)
Theorem e3722.. : ∀ x0 . 80242.. x0 ⟶ nIn (e4431.. x0) (7cb9a.. x0) (proof)
Theorem 35186.. : ∀ x0 . 80242.. x0 ⟶ prim1 (e4431.. x0) (45abd.. x0) (proof)
Theorem f3f53.. : ∀ x0 . 80242.. x0 ⟶ SNoEq_ (e4431.. x0) (7cb9a.. x0) x0 (proof)
Theorem aa41a.. : ∀ x0 . 80242.. x0 ⟶ SNoEq_ (e4431.. x0) (45abd.. x0) x0 (proof)
Theorem e3ccf.. : ∀ x0 . ordinal x0 ⟶ 80242.. x0 (proof)
Theorem aab4f.. : ∀ x0 . ordinal x0 ⟶ e4431.. x0 = x0 (proof)
Known 695d8.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ prim1 x2 x0
Known bba3d.. : ∀ x0 x1 . prim1 x0 x1 ⟶ nIn x1 x0
Theorem c0742.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) x0 ⟶ 099f3.. x1 x0 (proof)
Theorem 44eea.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ 099f3.. x1 x0 (proof)
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known ordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ordinal x1 ⟶ x0 x1
Theorem 09af0.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (4ae4a.. x0) ⟶ fe4bb.. x1 x0 (proof)
Known c79db.. : ∀ x0 . Subq x0 (4ae4a.. x0)
Theorem f1fea.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ Subq x0 x1 ⟶ fe4bb.. x0 x1 (proof)
Theorem 75c45.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 : ο . (∀ x2 x3 . 02b90.. x2 x3 ⟶ (∀ x4 . prim1 x4 x2 ⟶ prim1 (e4431.. x4) (e4431.. x0)) ⟶ (∀ x4 . prim1 x4 x3 ⟶ prim1 (e4431.. x4) (e4431.. x0)) ⟶ x0 = 02a50.. x2 x3 ⟶ x1) ⟶ x1 (proof)
Theorem cfea1.. : ∀ x0 : ι → ο . (∀ x1 x2 . 02b90.. x1 x2 ⟶ (∀ x3 . prim1 x3 x1 ⟶ x0 x3) ⟶ (∀ x3 . prim1 x3 x2 ⟶ x0 x3) ⟶ x0 (02a50.. x1 x2)) ⟶ ∀ x1 . 80242.. x1 ⟶ x0 x1 (proof)