Proofgold Address

Def 94e6a..^True : ο := ∀ x0 : ο . x0 ⟶ x0
Def 266ad..^False : ο := ∀ x0 : ο . x0
Def 0dc3c..^not : ο → ο := λ x0 : ο . x0 ⟶ False
Def 37da8..^and : ο → ο → ο := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Def 86ae6..^or : ο → ο → ο := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Def 6588e..^iff : ο → ο → ο := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known 1d1e5..^prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Def 31700..^Subq : ι → ι → ο := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known 21238..^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known 20faa..^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Def e69f9..^TransSet : ι → ο := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Def e45ed..^Union_closed : ι → ο := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ prim3 x1 ∈ x0
Def d2954..^Power_closed : ι → ο := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ prim4 x1 ∈ x0
Def 51353..^Repl_closed : ι → ο := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0) ⟶ prim5 x1 x2 ∈ x0
Def e1ecc..^ZF_closed : ι → ο := λ x0 . and (and (Union_closed x0) (Power_closed x0)) (Repl_closed x0)
Def 25345..^nIn : ι → ι → ο := λ x0 x1 . not (x0 ∈ x1)
Def 1b322..^nSubq : ι → ι → ο := λ x0 x1 . not (x0 ⊆ x1)
Known 0e736..^{UnivOf_ZF_closed} : ∀ x0 . ZF_closed (prim6 x0)
Known 3bf19..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 38267..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known 8d8e4..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known 4d966..^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Known 8349a..^EmptyE : ∀ x0 . nIn x0 0
Known eb5cb..^TrueI : True
Known 3c48d..^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Known 2faec..^Subq_Empty : ∀ x0 . 0 ⊆ x0
Known 7b673..^xm : ∀ x0 : ο . or x0 (not x0)
Known f9a23..^FalseE : False ⟶ ∀ x0 : ο . x0
Known 718be..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known c5df8..^pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Known cb999..^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known 50fab..^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Known ef907..^or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Known 827a9..^or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Known 3b7f5..^or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Known 2120c..^or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Known 906aa..^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Known d10b2..^or4I1 : ∀ x0 x1 x2 x3 : ο . x0 ⟶ or (or (or x0 x1) x2) x3
Known f9e4c..^or4I2 : ∀ x0 x1 x2 x3 : ο . x1 ⟶ or (or (or x0 x1) x2) x3
Known 1a588..^or4I3 : ∀ x0 x1 x2 x3 : ο . x2 ⟶ or (or (or x0 x1) x2) x3
Known 1ecd5..^or4I4 : ∀ x0 x1 x2 x3 : ο . x3 ⟶ or (or (or x0 x1) x2) x3
Known 1fdc2..^or4E : ∀ x0 x1 x2 x3 : ο . or (or (or x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x4) ⟶ (x1 ⟶ x4) ⟶ (x2 ⟶ x4) ⟶ (x3 ⟶ x4) ⟶ x4
Known 11fc4..^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Known 4e8f4..^or5I1 : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ or (or (or (or x0 x1) x2) x3) x4
Known 32035..^or5I2 : ∀ x0 x1 x2 x3 x4 : ο . x1 ⟶ or (or (or (or x0 x1) x2) x3) x4
Known 4aca8..^or5I3 : ∀ x0 x1 x2 x3 x4 : ο . x2 ⟶ or (or (or (or x0 x1) x2) x3) x4
Known 8e109..^or5I4 : ∀ x0 x1 x2 x3 x4 : ο . x3 ⟶ or (or (or (or x0 x1) x2) x3) x4
Known 59477..^or5I5 : ∀ x0 x1 x2 x3 x4 : ο . x4 ⟶ or (or (or (or x0 x1) x2) x3) x4
Known 780a9..^or5E : ∀ x0 x1 x2 x3 x4 : ο . or (or (or (or x0 x1) x2) x3) x4 ⟶ ∀ x5 : ο . (x0 ⟶ x5) ⟶ (x1 ⟶ x5) ⟶ (x2 ⟶ x5) ⟶ (x3 ⟶ x5) ⟶ (x4 ⟶ x5) ⟶ x5
Known a5dc2..^and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ and (and (and (and (and x0 x1) x2) x3) x4) x5
Known c8938..^and7I : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6
Known 41253..^and8I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7
Known 7c691..^and9I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8
Known 19e22..^and10I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9
Known 34224.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ x10 ⟶ and (and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9) x10
Known e679b.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ x10 ⟶ x11 ⟶ and (and (and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11
Known f9d7e.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ x10 ⟶ x11 ⟶ x12 ⟶ and (and (and (and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12
Known 5a186.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ x10 ⟶ x11 ⟶ x12 ⟶ x13 ⟶ and (and (and (and (and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13
Known 4e587.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ x10 ⟶ x11 ⟶ x12 ⟶ x13 ⟶ x14 ⟶ and (and (and (and (and (and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) x14
Known be87f.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ x10 ⟶ x11 ⟶ x12 ⟶ x13 ⟶ x14 ⟶ x15 ⟶ and (and (and (and (and (and (and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) x14) x15
Known 7b71b..^iff_refl : ∀ x0 : ο . iff x0 x0
Known 1a989..^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Known 6a283..^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Known a56fc..^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known 2efba..^Subq_ref : ∀ x0 . x0 ⊆ x0
Known fed66..^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known 98869..^{Empty_Subq_eq} : ∀ x0 . x0 ⊆ 0 ⟶ x0 = 0
Known 8b915..^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Known bade0..^UnionI : ∀ x0 x1 x2 . x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ x1 ∈ prim3 x0
Known 64707..^PowerE : ∀ x0 x1 . x1 ∈ prim4 x0 ⟶ x1 ⊆ x0
Known b7cc6..^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known f8498..^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known 34fef..^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known 0835b..^Repl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0
Known 78184..^ReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 = prim5 x0 x2
Param 1452f..^ordsucc : ι → ι
Known 3be80..^In_0_1 : 0 ∈ 1
Known 5a202..^In_0_2 : 0 ∈ 2
Known 431e9..^In_1_2 : 1 ∈ 2
Known 313d9..^In_0_3 : 0 ∈ 3
Known 8f3ce..^In_1_3 : 1 ∈ 3
Known ebdb5..^In_2_3 : 2 ∈ 3
Known 2d416..^In_0_4 : 0 ∈ 4
Known 1e2d5..^In_1_4 : 1 ∈ 4
Known 2cbb9..^In_2_4 : 2 ∈ 4
Known 22a0a..^In_3_4 : 3 ∈ 4
Known 965bc..^In_0_5 : 0 ∈ 5
Known 34c02..^In_1_5 : 1 ∈ 5
Known 7ed8e..^In_2_5 : 2 ∈ 5
Known df92f..^In_3_5 : 3 ∈ 5
Known 03b9f..^In_4_5 : 4 ∈ 5
Known c6f0c..^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Known 74563..^cases_2 : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Known 1a8a2..^cases_3 : ∀ x0 . x0 ∈ 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
Known 58ec1..^cases_4 : ∀ x0 . x0 ∈ 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Known f3805..^cases_5 : ∀ x0 . x0 ∈ 5 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 x0