Proofgold Address

Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem iff_refl : ∀ x0 : ο . iff x0 x0 (proof)
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem iff_sym : ∀ x0 x1 : ο . iff x0 x1 ⟶ iff x1 x0 (proof)
Theorem iff_trans : ∀ x0 x1 x2 : ο . iff x0 x1 ⟶ iff x1 x2 ⟶ iff x0 x2 (proof)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem not_or_and_demorgan : ∀ x0 x1 : ο . not (or x0 x1) ⟶ and (not x0) (not x1) (proof)
Theorem and_not_or_demorgan : ∀ x0 x1 : ο . and (not x0) (not x1) ⟶ not (or x0 x1) (proof)
Theorem not_ex_all_demorgan_i : ∀ x0 : ι → ο . not (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ ∀ x1 . not (x0 x1) (proof)
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem not_all_ex_demorgan_i : ∀ x0 : ι → ο . not (∀ x1 . x0 x1) ⟶ ∀ x1 : ο . (∀ x2 . not (x0 x2) ⟶ x1) ⟶ x1 (proof)
Known prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known xm : ∀ x0 : ο . or x0 (not x0)
Theorem eq_or_nand : or = λ x1 x2 : ο . not (and (not x1) (not x2)) (proof)
Definition EpsR_i_i_1 := λ x0 : ι → ι → ο . prim0 (λ x1 . ∀ x2 : ο . (∀ x3 . x0 x1 x3 ⟶ x2) ⟶ x2)
Definition EpsR_i_i_2 := λ x0 : ι → ι → ο . prim0 (x0 (EpsR_i_i_1 x0))
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem EpsR_i_i_12 : ∀ x0 : ι → ι → ο . (∀ x1 : ο . (∀ x2 . (∀ x3 : ο . (∀ x4 . x0 x2 x4 ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) ⟶ x0 (EpsR_i_i_1 x0) (EpsR_i_i_2 x0) (proof)
Definition DescrR_i_io_1 := λ x0 : ι → (ι → ο) → ο . prim0 (λ x1 . and (∀ x2 : ο . (∀ x3 : ι → ο . x0 x1 x3 ⟶ x2) ⟶ x2) (∀ x2 x3 : ι → ο . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x2 = x3))
Param Descr_Vo1 : ((ι → ο) → ο) → ι → ο
Definition DescrR_i_io_2 := λ x0 : ι → (ι → ο) → ο . Descr_Vo1 (x0 (DescrR_i_io_1 x0))
Known Descr_Vo1_prop : ∀ x0 : (ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo1 x0)
Theorem DescrR_i_io_12 : ∀ x0 : ι → (ι → ο) → ο . (∀ x1 : ο . (∀ x2 . and (∀ x3 : ο . (∀ x4 : ι → ο . x0 x2 x4 ⟶ x3) ⟶ x3) (∀ x3 x4 : ι → ο . x0 x2 x3 ⟶ x0 x2 x4 ⟶ x3 = x4) ⟶ x1) ⟶ x1) ⟶ x0 (DescrR_i_io_1 x0) (DescrR_i_io_2 x0) (proof)
Definition PNoEq_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)
Theorem PNoEq_ref_ : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 x1 (proof)
Theorem PNoEq_sym_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x1 (proof)
Theorem PNoEq_tra_ : ∀ x0 . ∀ x1 x2 x3 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x3 ⟶ PNoEq_ x0 x1 x3 (proof)
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Theorem PNoEq_antimon_ : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . prim1 x3 x2 ⟶ PNoEq_ x2 x0 x1 ⟶ PNoEq_ x3 x0 x1 (proof)
Definition PNoLt_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (and (and (PNoEq_ x4 x1 x2) (not (x1 x4))) (x2 x4)) ⟶ x3) ⟶ x3
Theorem 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 (proof)
Theorem PNoLt_irref_ : ∀ x0 . ∀ x1 : ι → ο . not (PNoLt_ x0 x1 x1) (proof)
Theorem PNoLt_mon_ : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . prim1 x3 x2 ⟶ PNoLt_ x3 x0 x1 ⟶ PNoLt_ x2 x0 x1 (proof)
Known ordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ordinal x1 ⟶ x0 x1
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Theorem PNoLt_trichotomy_or_ : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) (proof)
Known ordinal_trichotomy_or : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (prim1 x0 x1) (x0 = x1)) (prim1 x1 x0)
Known ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1
Theorem PNoLt_tra_ : ∀ x0 . ordinal x0 ⟶ ∀ x1 x2 x3 : ι → ο . PNoLt_ x0 x1 x2 ⟶ PNoLt_ x0 x2 x3 ⟶ PNoLt_ x0 x1 x3 (proof)
Param d3786.. : ι → ι → ι
Definition 40dde.. := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (or (PNoLt_ (d3786.. x0 x2) x1 x3) (and (and (prim1 x0 x2) (PNoEq_ x0 x1 x3)) (x3 x0))) (and (and (prim1 x2 x0) (PNoEq_ x2 x1 x3)) (not (x1 x2)))
Known or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Theorem d5535.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt_ (d3786.. x0 x1) x2 x3 ⟶ 40dde.. x0 x2 x1 x3 (proof)
Known or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Theorem 0f47f.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . prim1 x0 x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ 40dde.. x0 x2 x1 x3 (proof)
Known or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Theorem 27954.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . prim1 x1 x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ 40dde.. x0 x2 x1 x3 (proof)
Theorem 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 (proof)
Known 5cae2.. : ∀ x0 . d3786.. x0 x0 = x0
Known In_irref : ∀ x0 . nIn x0 x0
Theorem 60396.. : ∀ x0 . ∀ x1 x2 : ι → ο . 40dde.. x0 x1 x0 x2 ⟶ PNoLt_ x0 x1 x2 (proof)
Theorem 7de10.. : ∀ x0 . ∀ x1 : ι → ο . not (40dde.. x0 x1 x0 x1) (proof)
Known bd118.. : ∀ x0 x1 . Subq x0 x1 ⟶ d3786.. x0 x1 = x0
Known Subq_ref : ∀ x0 . Subq x0 x0
Known d7325.. : ∀ x0 x1 . d3786.. x0 x1 = d3786.. x1 x0
Known dec57.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (d3786.. x0 x1)
Theorem 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) (proof)
Known 3eff2.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ and (prim1 x2 x0) (prim1 x2 x1)
Known iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1
Theorem 43fd7.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . 40dde.. x0 x2 x1 x3 ⟶ PNoEq_ x1 x3 x4 ⟶ 40dde.. x0 x2 x1 x4 (proof)
Theorem 1f4e8.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoEq_ x0 x2 x3 ⟶ 40dde.. x0 x3 x1 x4 ⟶ 40dde.. x0 x2 x1 x4 (proof)
Known 2d07f.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 x1 ⟶ prim1 x2 (d3786.. x0 x1)
Theorem 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 (proof)
Definition 35b9b.. := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (40dde.. x0 x1 x2 x3) (and (x0 = x2) (PNoEq_ x0 x1 x3))
Theorem 8fc51.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 40dde.. x0 x2 x1 x3 ⟶ 35b9b.. x0 x2 x1 x3 (proof)
Theorem a40a2.. : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2 ⟶ 35b9b.. x0 x1 x0 x2 (proof)
Theorem fb736.. : ∀ x0 . ∀ x1 : ι → ο . 35b9b.. x0 x1 x0 x1 (proof)
Theorem 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) (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem da030.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoEq_ x0 x2 x3 ⟶ 35b9b.. x0 x3 x1 x4 ⟶ 35b9b.. x0 x2 x1 x4 (proof)
Theorem 421fb.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . 35b9b.. x0 x2 x1 x3 ⟶ PNoEq_ x1 x3 x4 ⟶ 35b9b.. x0 x2 x1 x4 (proof)
Theorem 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 (proof)
Definition 8356a.. := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (ordinal x4) (∀ x5 : ο . (∀ x6 : ι → ο . and (x0 x4 x6) (35b9b.. x1 x2 x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Definition 610d8.. := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (ordinal x4) (∀ x5 : ο . (∀ x6 : ι → ο . and (x0 x4 x6) (35b9b.. x4 x6 x1 x2) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Theorem 76c44.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 x2 . ∀ x3 x4 : ι → ο . ordinal x1 ⟶ ordinal x2 ⟶ 8356a.. x0 x1 x3 ⟶ 35b9b.. x2 x4 x1 x3 ⟶ 8356a.. x0 x2 x4 (proof)
Theorem 46c67.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . x0 x1 x2 ⟶ 8356a.. x0 x1 x2 (proof)
Theorem ddfe3.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . x0 x1 x2 ⟶ 610d8.. x0 x1 x2 (proof)
Theorem 49ea3.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 x2 . ∀ x3 x4 : ι → ο . ordinal x1 ⟶ ordinal x2 ⟶ 610d8.. x0 x1 x3 ⟶ 35b9b.. x1 x3 x2 x4 ⟶ 610d8.. x0 x2 x4 (proof)
Definition ed32f.. := λ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . x0 x2 x3 ⟶ ∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x1 x4 x5 ⟶ 40dde.. x2 x3 x4 x5
Theorem 0779e.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ed32f.. (8356a.. x0) (610d8.. x1) (proof)
Definition 6f2c4.. := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ι → ο . 8356a.. x0 x3 x4 ⟶ 40dde.. x3 x4 x1 x2
Definition dafc2.. := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ι → ο . 610d8.. x0 x3 x4 ⟶ 40dde.. x1 x2 x3 x4
Definition 8033b.. := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (6f2c4.. x0 x2 x3) (dafc2.. x1 x2 x3)
Theorem 7132a.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3 ⟶ 6f2c4.. x0 x1 x2 ⟶ 6f2c4.. x0 x1 x3 (proof)
Known bba3d.. : ∀ x0 x1 . prim1 x0 x1 ⟶ nIn x1 x0
Theorem 696cf.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x1 ⟶ 6f2c4.. x0 x1 x2 ⟶ 6f2c4.. x0 x3 x2 (proof)
Theorem 504aa.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3 ⟶ dafc2.. x0 x1 x2 ⟶ dafc2.. x0 x1 x3 (proof)
Theorem 649ba.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x1 ⟶ dafc2.. x0 x1 x2 ⟶ dafc2.. x0 x3 x2 (proof)
Theorem e4d06.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 x4 : ι → ο . PNoEq_ x2 x3 x4 ⟶ 8033b.. x0 x1 x2 x3 ⟶ 8033b.. x0 x1 x2 x4 (proof)
Theorem 0b627.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x2 ⟶ 8033b.. x0 x1 x2 x3 ⟶ 8033b.. x0 x1 x4 x3 (proof)
Definition 078b6.. := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (8033b.. x0 x1 x2 x3) (∀ x4 : ι → ο . 8033b.. x0 x1 x2 x4 ⟶ PNoEq_ x2 x3 x4)
Param 4ae4a.. : ι → ι
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)))
Theorem PNo_extend0_eq : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . and (x1 x2) (x2 = x0 ⟶ ∀ x3 : ο . x3)) (proof)
Theorem PNo_extend1_eq : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . or (x1 x2) (x2 = x0)) (proof)
Known 74eef.. : ∀ x0 . ordinal x0 ⟶ or (∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) x0) (∀ x1 : ο . (∀ x2 . and (prim1 x2 x0) (x0 = 4ae4a.. x2) ⟶ x1) ⟶ x1)
Known iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0
Known 5faa3.. : ∀ x0 . prim1 x0 (4ae4a.. x0)
Known 09068.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) (4ae4a.. x0)
Known b72a3.. : ∀ x0 . ordinal x0 ⟶ ordinal (4ae4a.. x0)
Known 4f62a.. : ∀ x0 x1 . ordinal x0 ⟶ prim1 x1 x0 ⟶ or (prim1 (4ae4a.. x1) x0) (x0 = 4ae4a.. x1)
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Known c79db.. : ∀ x0 . Subq x0 (4ae4a.. x0)
Theorem c0216.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ or (∀ x3 : ο . (∀ x4 : ι → ο . 078b6.. x0 x1 x2 x4 ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (prim1 x4 x2) (∀ x5 : ο . (∀ x6 : ι → ο . a59df.. x0 x1 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) (proof)
Definition PNo_lenbdd := λ x0 . λ x1 : ι → (ι → ο) → ο . ∀ x2 . ∀ x3 : ι → ο . x1 x2 x3 ⟶ prim1 x2 x0
Theorem e3fc6.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . 8033b.. x0 x1 x2 x3 ⟶ 8033b.. x0 x1 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)) (proof)
Theorem 47a05.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . 8033b.. x0 x1 x2 x3 ⟶ 8033b.. x0 x1 (4ae4a.. x2) (λ x4 . or (x3 x4) (x4 = x2)) (proof)
Theorem 7a19c.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . 8033b.. x0 x1 x2 x3 ⟶ a59df.. x0 x1 x2 x3 (proof)
Theorem f23bc.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 (4ae4a.. x2)) (∀ x5 : ο . (∀ x6 : ι → ο . a59df.. x0 x1 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
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)
Theorem 654c3.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3 ⟶ cae4c.. x0 x1 x2 ⟶ cae4c.. x0 x1 x3 (proof)
Theorem 04247.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3 ⟶ bc2b0.. x0 x1 x2 ⟶ bc2b0.. x0 x1 x3 (proof)
Theorem dfc25.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 x4 : ι → ο . PNoEq_ x2 x3 x4 ⟶ 47618.. x0 x1 x2 x3 ⟶ 47618.. x0 x1 x2 x4 (proof)
Theorem 2042e.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 . prim1 x2 (4ae4a.. x1) ⟶ ∀ x3 : ι → ο . cae4c.. x0 x1 x3 ⟶ 6f2c4.. x0 x2 x3 (proof)
Theorem 2df7d.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 . prim1 x2 (4ae4a.. x1) ⟶ ∀ x3 : ι → ο . bc2b0.. x0 x1 x3 ⟶ dafc2.. x0 x2 x3 (proof)
Theorem 45f48.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . prim1 x3 (4ae4a.. x2) ⟶ ∀ x4 : ι → ο . 47618.. x0 x1 x2 x4 ⟶ 8033b.. x0 x1 x3 x4 (proof)
Theorem 61193.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . a59df.. x0 x1 x2 x3 ⟶ 47618.. x0 x1 x2 x3 (proof)
Theorem 48a9a.. : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . (∀ x4 . prim1 x4 x2 ⟶ x3 x4) ⟶ (∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x0 x4 x5 ⟶ prim1 x4 x2) ⟶ (∀ x4 . prim1 x4 x2 ⟶ x0 x4 x3) ⟶ (∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . not (x1 x4 x5)) ⟶ 47618.. x0 x1 x2 x3 (proof)
Theorem 92acb.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 (4ae4a.. x2)) (∀ x5 : ο . (∀ x6 : ι → ο . 47618.. x0 x1 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
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 least_ordinal_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2) ⟶ x1) ⟶ x1) ⟶ ∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . prim1 x3 x2 ⟶ not (x0 x3)) ⟶ x1) ⟶ x1
Theorem de2f8.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 : ι → ο . 1a487.. x0 x1 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Definition ced99.. := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (1a487.. x0 x1 x2 x3) (∀ x4 . nIn x4 x2 ⟶ not (x3 x4))
Theorem f2429.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ ∀ x3 x4 : ι → ο . 1a487.. x0 x1 x2 x3 ⟶ 47618.. x0 x1 x2 x4 ⟶ ∀ x5 . prim1 x5 x2 ⟶ iff (x3 x5) (x4 x5) (proof)
Known pred_ext : ∀ x0 x1 : ι → ο . (∀ x2 . iff (x0 x2) (x1 x2)) ⟶ x0 = x1
Theorem 8116c.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (∀ x5 : ο . (∀ x6 : ι → ο . ced99.. x0 x1 x4 x6 ⟶ x5) ⟶ x5) (∀ x5 x6 : ι → ο . ced99.. x0 x1 x4 x5 ⟶ ced99.. x0 x1 x4 x6 ⟶ x5 = x6) ⟶ x3) ⟶ x3 (proof)
Definition 7b9f3.. := λ x0 x1 : ι → (ι → ο) → ο . DescrR_i_io_1 (ced99.. x0 x1)
Definition ce2d5.. := λ x0 x1 : ι → (ι → ο) → ο . DescrR_i_io_2 (ced99.. x0 x1)
Theorem 67865.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ced99.. x0 x1 (7b9f3.. x0 x1) (ce2d5.. x0 x1) (proof)
Theorem 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) (proof)
Theorem caca6.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ordinal (7b9f3.. x0 x1) (proof)
Theorem 56572.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ 47618.. x0 x1 (7b9f3.. x0 x1) (ce2d5.. x0 x1) (proof)
Theorem 01c28.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 . prim1 x3 (7b9f3.. x0 x1) ⟶ ∀ x4 : ι → ο . not (47618.. x0 x1 x3 x4) (proof)
Known ordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (prim1 x0 x1) (Subq x1 x0)
Theorem 00673.. : ∀ x0 x1 : ι → (ι → ο) → ο . ed32f.. x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ prim1 (7b9f3.. x0 x1) (4ae4a.. x2) (proof)
Definition 7eb85.. := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . and (prim1 x2 x0) (40dde.. x2 x3 x0 x1)
Definition 0dfb2.. := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . and (prim1 x2 x0) (40dde.. x0 x1 x2 x3)
Theorem a34ea.. : ∀ x0 . ∀ x1 : ι → ο . PNo_lenbdd x0 (7eb85.. x0 x1) (proof)
Theorem f50a4.. : ∀ x0 . ∀ x1 : ι → ο . PNo_lenbdd x0 (0dfb2.. x0 x1) (proof)
Theorem 83944.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . ed32f.. (7eb85.. x0 x1) (0dfb2.. x0 x1) (proof)
Theorem 92f73.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . 47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x0 x1 (proof)
Theorem 9524b.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . 7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1) = x0 (proof)
Theorem f1225.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNoEq_ x0 x1 (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) (proof)