Proofgold Address

Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2 (proof)
Theorem and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2 (proof)
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2 (proof)
Theorem or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2 (proof)
Theorem or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3 (proof)
Theorem and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3 (proof)
Theorem and4E : ∀ x0 x1 x2 x3 : ο . and (and (and x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4) ⟶ x4 (proof)
Theorem or4I1 : ∀ x0 x1 x2 x3 : ο . x0 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem or4I2 : ∀ x0 x1 x2 x3 : ο . x1 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem or4I3 : ∀ x0 x1 x2 x3 : ο . x2 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem or4I4 : ∀ x0 x1 x2 x3 : ο . x3 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem or4E : ∀ x0 x1 x2 x3 : ο . or (or (or x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x4) ⟶ (x1 ⟶ x4) ⟶ (x2 ⟶ x4) ⟶ (x3 ⟶ x4) ⟶ x4 (proof)
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known 0ddd1.. : ∀ x0 x1 . (∀ x2 . iff (prim1 x2 x0) (prim1 x2 x1)) ⟶ x0 = x1
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1 (proof)
Theorem Subq_ref : ∀ x0 . Subq x0 x0 (proof)
Theorem Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2 (proof)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Known xm : ∀ x0 : ο . or x0 (not x0)
Known FalseE : False ⟶ ∀ x0 : ο . x0
Theorem dneg : ∀ x0 : ο . not (not x0) ⟶ x0 (proof)
Param 4a7ef.. : ι
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 2b26f.. : not (∀ x0 : ο . (∀ x1 . prim1 x1 4a7ef.. ⟶ x0) ⟶ x0) (proof)
Theorem e8942.. : ∀ x0 . Subq 4a7ef.. x0 (proof)
Param c2e41.. : ι → ι → ο
Known adb47.. : ∀ x0 . ∀ x1 : ο . (∀ x2 . and (and (and (prim1 x0 x2) (∀ x3 x4 . prim1 x3 x2 ⟶ Subq x4 x3 ⟶ prim1 x4 x2)) (∀ x3 . prim1 x3 x2 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x2) (∀ x6 . Subq x6 x3 ⟶ prim1 x6 x5) ⟶ x4) ⟶ x4)) (∀ x3 . Subq x3 x2 ⟶ or (c2e41.. x3 x2) (prim1 x3 x2)) ⟶ x1) ⟶ x1
Param 1216a.. : ι → (ι → ο) → ι
Known 492ff.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ ∀ x3 : ο . (prim1 x2 x0 ⟶ x1 x2 ⟶ x3) ⟶ x3
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Theorem b0a2d.. : ∀ x0 . ∀ x1 : ο . (∀ x2 . (∀ x3 . iff (prim1 x3 x2) (Subq x3 x0)) ⟶ x1) ⟶ x1 (proof)
Definition e5b72.. := λ x0 . prim0 (λ x1 . ∀ x2 . iff (prim1 x2 x1) (Subq x2 x0))
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem cf34a.. : ∀ x0 x1 . iff (prim1 x1 (e5b72.. x0)) (Subq x1 x0) (proof)
Theorem b21da.. : ∀ x0 x1 . prim1 x1 (e5b72.. x0) ⟶ Subq x1 x0 (proof)
Theorem 3daee.. : ∀ x0 x1 . Subq x1 x0 ⟶ prim1 x1 (e5b72.. x0) (proof)
Theorem 72294.. : ∀ x0 x1 . Subq x0 x1 ⟶ Subq (e5b72.. x0) (e5b72.. x1) (proof)
Theorem c5d9a.. : ∀ x0 . prim1 4a7ef.. (e5b72.. x0) (proof)
Theorem 62c05.. : ∀ x0 . prim1 x0 (e5b72.. x0) (proof)
Definition 0ac37.. := λ x0 x1 . prim3 (prim2 x0 x1)
Known UnionI : ∀ x0 x1 x2 . prim1 x1 x2 ⟶ prim1 x2 x0 ⟶ prim1 x1 (prim3 x0)
Known 67787.. : ∀ x0 x1 . prim1 x0 (prim2 x0 x1)
Theorem da962.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 (0ac37.. x0 x1) (proof)
Known 5a932.. : ∀ x0 x1 . prim1 x1 (prim2 x0 x1)
Theorem 287ca.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 x2 (0ac37.. x0 x1) (proof)
Known UnionE_impred : ∀ x0 x1 . prim1 x1 (prim3 x0) ⟶ ∀ x2 : ο . (∀ x3 . prim1 x1 x3 ⟶ prim1 x3 x0 ⟶ x2) ⟶ x2
Known 2532b.. : ∀ x0 x1 x2 . prim1 x0 (prim2 x1 x2) ⟶ or (x0 = x1) (x0 = x2)
Theorem edd11.. : ∀ x0 x1 x2 . prim1 x2 (0ac37.. x0 x1) ⟶ or (prim1 x2 x0) (prim1 x2 x1) (proof)
Known 6982e.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ and (prim1 x2 x0) (x1 x2)
Theorem d0a1f.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ prim1 x2 x0 (proof)
Theorem ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2 (proof)
Definition d3786.. := λ x0 x1 . 1216a.. x0 (λ x2 . prim1 x2 x1)
Theorem 2d07f.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 x1 ⟶ prim1 x2 (d3786.. x0 x1) (proof)
Theorem 3eff2.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ and (prim1 x2 x0) (prim1 x2 x1) (proof)
Theorem 695d8.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ prim1 x2 x0 (proof)
Theorem a5fe0.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ prim1 x2 x1 (proof)
Param 91630.. : ι → ι
Definition 4ae4a.. := λ x0 . 0ac37.. x0 (91630.. x0)
Theorem c79db.. : ∀ x0 . Subq x0 (4ae4a.. x0) (proof)
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Theorem 5faa3.. : ∀ x0 . prim1 x0 (4ae4a.. x0) (proof)
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Theorem 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0) (proof)
Known 113d7.. : ∀ x0 x1 . prim1 x1 x0 ⟶ ∀ x2 : ο . (∀ x3 . and (prim1 x3 x0) (not (∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (prim1 x5 x3) ⟶ x4) ⟶ x4)) ⟶ x2) ⟶ x2
Theorem bba3d.. : ∀ x0 x1 . prim1 x0 x1 ⟶ nIn x1 x0 (proof)
Theorem efbae.. : ∀ x0 . 4a7ef.. = 4ae4a.. x0 ⟶ ∀ x1 : ο . x1 (proof)
Theorem 1b1d1.. : ∀ x0 . 4ae4a.. x0 = 4a7ef.. ⟶ ∀ x1 : ο . x1 (proof)
Theorem 054cd.. : ∀ x0 x1 . 4ae4a.. x0 = 4ae4a.. x1 ⟶ x0 = x1 (proof)
Theorem 4b095.. : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ 4ae4a.. x0 = 4ae4a.. x1 ⟶ ∀ x2 : ο . x2 (proof)
Theorem f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..) (proof)
Theorem 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Known andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Theorem ordinal_TransSet : ∀ x0 . ordinal x0 ⟶ TransSet x0 (proof)
Known andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem ordinal_In_TransSet : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ TransSet x1 (proof)
Theorem 40f7a.. : ordinal 4a7ef.. (proof)
Theorem ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1 (proof)
Definition ba9d8.. := λ x0 . ∀ x1 : ι → ο . x1 4a7ef.. ⟶ (∀ x2 . x1 x2 ⟶ x1 (4ae4a.. x2)) ⟶ x1 x0
Theorem 4c9b8.. : ba9d8.. 4a7ef.. (proof)
Theorem 2fbbc.. : ∀ x0 . ba9d8.. x0 ⟶ ba9d8.. (4ae4a.. x0) (proof)
Theorem 3db81.. : ba9d8.. (4ae4a.. 4a7ef..) (proof)
Theorem d7fe6.. : ba9d8.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem 26358.. : ∀ x0 . ba9d8.. x0 ⟶ prim1 4a7ef.. (4ae4a.. x0) (proof)
Theorem 3238a.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) (4ae4a.. x0) (proof)
Theorem 5c211.. : ∀ x0 : ι → ο . x0 4a7ef.. ⟶ (∀ x1 . ba9d8.. x1 ⟶ x0 x1 ⟶ x0 (4ae4a.. x1)) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1 (proof)
Theorem be77e.. : ∀ x0 . ba9d8.. x0 ⟶ or (x0 = 4a7ef..) (∀ x1 : ο . (∀ x2 . and (ba9d8.. x2) (x0 = 4ae4a.. x2) ⟶ x1) ⟶ x1) (proof)
Theorem 839f4.. : ∀ x0 : ι → ο . (∀ x1 . ba9d8.. x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1 (proof)
Theorem 10a0b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ba9d8.. x1 (proof)
Theorem 8f913.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0 (proof)
Theorem 82e3b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 (4ae4a.. x0) ⟶ Subq x1 x0 (proof)
Theorem a1a9f.. : ∀ x0 . TransSet x0 ⟶ TransSet (4ae4a.. x0) (proof)
Theorem b72a3.. : ∀ x0 . ordinal x0 ⟶ ordinal (4ae4a.. x0) (proof)
Theorem f3fb5.. : ∀ x0 . ba9d8.. x0 ⟶ ordinal x0 (proof)
Theorem 4114a.. : ∀ x0 : ο . (∀ x1 . (∀ x2 . iff (prim1 x2 x1) (ba9d8.. x2)) ⟶ x0) ⟶ x0 (proof)
Definition 48ef8.. := prim0 (λ x0 . ∀ x1 . iff (prim1 x1 x0) (ba9d8.. x1))
Theorem 6c085.. : ∀ x0 . iff (prim1 x0 48ef8..) (ba9d8.. x0) (proof)
Theorem c2711.. : ∀ x0 . prim1 x0 48ef8.. ⟶ ba9d8.. x0 (proof)
Theorem a3321.. : ∀ x0 . ba9d8.. x0 ⟶ prim1 x0 48ef8.. (proof)
Theorem 8ee89.. : prim1 4a7ef.. 48ef8.. (proof)
Theorem 98ac3.. : ∀ x0 . prim1 x0 48ef8.. ⟶ prim1 (4ae4a.. x0) 48ef8.. (proof)
Definition aa8d2.. := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . x3 4a7ef.. x1 ⟶ (∀ x4 . ba9d8.. x4 ⟶ ∀ x5 . x3 x4 x5 ⟶ x3 (4ae4a.. x4) (prim3 x5)) ⟶ x3 x0 x2
Theorem 4a672.. : ∀ x0 . aa8d2.. 4a7ef.. x0 x0 (proof)
Theorem b5347.. : ∀ x0 x1 . ba9d8.. x1 ⟶ ∀ x2 . aa8d2.. x1 x0 x2 ⟶ aa8d2.. (4ae4a.. x1) x0 (prim3 x2) (proof)
Theorem ac124.. : ∀ x0 . ∀ x1 : ι → ι → ο . x1 4a7ef.. x0 ⟶ (∀ x2 . ba9d8.. x2 ⟶ ∀ x3 . aa8d2.. x2 x0 x3 ⟶ x1 x2 x3 ⟶ x1 (4ae4a.. x2) (prim3 x3)) ⟶ ∀ x2 x3 . ba9d8.. x2 ⟶ aa8d2.. x2 x0 x3 ⟶ x1 x2 x3 (proof)
Theorem 5f7ef.. : ∀ x0 x1 x2 . ba9d8.. x1 ⟶ aa8d2.. x1 x0 x2 ⟶ or (and (x1 = 4a7ef..) (x2 = x0)) (∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (and (x1 = 4ae4a.. x4) (x2 = prim3 x6)) (aa8d2.. x4 x0 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) (proof)
Theorem a87f5.. : ∀ x0 x1 . aa8d2.. 4a7ef.. x0 x1 ⟶ x1 = x0 (proof)
Theorem f1d4d.. : ∀ x0 x1 x2 . ba9d8.. x0 ⟶ aa8d2.. (4ae4a.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (x2 = prim3 x4) (aa8d2.. x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 8312b.. : ∀ x0 x1 . ba9d8.. x1 ⟶ ∀ x2 : ο . (∀ x3 . aa8d2.. x1 x0 x3 ⟶ x2) ⟶ x2 (proof)
Theorem 0cbec.. : ∀ x0 x1 . ba9d8.. x1 ⟶ ∀ x2 x3 . aa8d2.. x1 x0 x2 ⟶ aa8d2.. x1 x0 x3 ⟶ x2 = x3 (proof)
Theorem 3e6f6.. : ∀ x0 x1 . ba9d8.. x0 ⟶ aa8d2.. x0 x1 (prim0 (aa8d2.. x0 x1)) (proof)
Theorem 2cb0a.. : ∀ x0 . prim0 (aa8d2.. 4a7ef.. x0) = x0 (proof)
Theorem 057f4.. : ∀ x0 x1 . ba9d8.. x0 ⟶ prim0 (aa8d2.. (4ae4a.. x0) x1) = prim3 (prim0 (aa8d2.. x0 x1)) (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Definition 2f2ea.. := λ x0 . prim3 (94f9e.. 48ef8.. (λ x1 . prim0 (aa8d2.. x1 x0)))
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem 7fd4e.. : ∀ x0 x1 x2 . ba9d8.. x2 ⟶ prim1 x1 (prim0 (aa8d2.. x2 x0)) ⟶ prim1 x1 (2f2ea.. x0) (proof)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem 45a0f.. : ∀ x0 x1 . prim1 x1 (2f2ea.. x0) ⟶ ∀ x2 : ο . (∀ x3 . ba9d8.. x3 ⟶ prim1 x1 (prim0 (aa8d2.. x3 x0)) ⟶ x2) ⟶ x2 (proof)
Theorem 96add.. : ∀ x0 . Subq x0 (2f2ea.. x0) (proof)
Theorem fb6d0.. : ∀ x0 . TransSet (2f2ea.. x0) (proof)
Theorem In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1 (proof)