Proofgold Asset

Param nat_p^nat_p : ι → ο
Param ordsucc^ordsucc : ι → ι
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Param Sing^Sing : ι → ι
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Known In_0_1^In_0_1 : 0 ∈ 1
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Theorem not_TransSet_Sing_tagn^{not_TransSet_Sing_tagn} : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ not (TransSet (Sing x0)) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition ordinal^ordinal := λ x0 . and (TransSet x0) (∀ x1 . x1 ∈ x0 ⟶ TransSet x1)
Theorem not_ordinal_Sing_tagn^{not_ordinal_Sing_tagn} : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ not (ordinal (Sing x0)) (proof)
Param binunion^binunion : ι → ι → ι
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Known ordinal_Hered^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordinal x1
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Theorem c383e.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 . not (ordinal (SetAdjoin x1 (Sing x0))) (proof)
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Theorem 1a4b4.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 . ordinal x1 ⟶ nIn (SetAdjoin x2 (Sing x0)) x1 (proof)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Theorem 292f1.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ nIn (Sing x0) (Sing (Sing 1)) (proof)
Param SNo^SNo : ι → ο
Param SNoLev^SNoLev : ι → ι
Definition SNoElts_^SNoElts_ := λ x0 . binunion x0 {SetAdjoin x1 (Sing 1)|x1 ∈ x0}
Param exactly1of2^exactly1of2 : ο → ο → ο
Definition SNo_^SNo_ := λ x0 x1 . and (x1 ⊆ SNoElts_ x0) (∀ x2 . x2 ∈ x0 ⟶ exactly1of2 (SetAdjoin x2 (Sing 1) ∈ x1) (x2 ∈ x1))
Known SNoLev_prop^SNoLev_prop : ∀ x0 . SNo x0 ⟶ and (ordinal (SNoLev x0)) (SNo_ (SNoLev x0) x0)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem 3bbaa.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 . SNo x1 ⟶ nIn (SetAdjoin x2 (Sing x0)) x1 (proof)
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Theorem 799ec.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 . SNo x1 ⟶ SNo x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x2 ⟶ SetAdjoin x3 (Sing x0) = SetAdjoin x4 (Sing x0) ⟶ x3 ⊆ x4 (proof)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Theorem 8244d.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 . SNo x1 ⟶ SNo x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x2 ⟶ SetAdjoin x3 (Sing x0) = SetAdjoin x4 (Sing x0) ⟶ x3 = x4 (proof)
Definition e9c39.. := λ x0 x1 x2 . binunion x1 {SetAdjoin x3 (Sing x0)|x3 ∈ x2}
Theorem 71aee.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 x3 x4 . SNo x1 ⟶ e9c39.. x0 x1 x2 = e9c39.. x0 x3 x4 ⟶ x1 ⊆ x3 (proof)
Theorem 0efc6.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 x3 x4 . SNo x1 ⟶ SNo x3 ⟶ e9c39.. x0 x1 x2 = e9c39.. x0 x3 x4 ⟶ x1 = x3 (proof)
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Theorem 8e0ee.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 x3 x4 . SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ e9c39.. x0 x1 x2 = e9c39.. x0 x3 x4 ⟶ x2 ⊆ x4 (proof)
Theorem 37675.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 x3 x4 . SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ e9c39.. x0 x1 x2 = e9c39.. x0 x3 x4 ⟶ x2 = x4 (proof)
Known Repl_Empty^Repl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0
Known binunion_idr^binunion_idr : ∀ x0 . binunion x0 0 = x0
Theorem 3d28a.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 . e9c39.. x0 x1 0 = x1 (proof)
Definition ad280.. := e9c39.. 2
Known nat_2^nat_2 : nat_p 2
Known In_1_2^In_1_2 : 1 ∈ 2
Theorem 43bcd.. : ∀ x0 . ad280.. x0 0 = x0 (proof)
Theorem 8ae5d.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x2 ⟶ ad280.. x0 x1 = ad280.. x2 x3 ⟶ x0 = x2 (proof)
Theorem 943f5.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ ad280.. x0 x1 = ad280.. x2 x3 ⟶ x1 = x3 (proof)
Definition c7ce4.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (x0 = ad280.. x2 x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem e4080.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ c7ce4.. (ad280.. x0 x1) (proof)
Theorem 3577c.. : ∀ x0 . c7ce4.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 . SNo x2 ⟶ SNo x3 ⟶ x0 = ad280.. x2 x3 ⟶ x1 (ad280.. x2 x3)) ⟶ x1 x0 (proof)
Known SNo_0^SNo_0 : SNo 0
Theorem 2c33a.. : ∀ x0 . SNo x0 ⟶ c7ce4.. x0 (proof)
Theorem Sing_inj^Sing_inj : ∀ x0 x1 . Sing x0 = Sing x1 ⟶ x0 = x1 (proof)
Definition 68498.. := λ x0 x1 . ∀ x2 . x2 ∈ x1 ⟶ ∀ x3 : ο . (∀ x4 . and (SNo x4) (or (x2 ∈ x4) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x4) (∀ x7 : ο . (∀ x8 . and (x8 ∈ x0) (and (1 ∈ x8) (x2 = SetAdjoin x6 (Sing x8))) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ x3) ⟶ x3
Known SNoLev_^SNoLev_ : ∀ x0 . SNo x0 ⟶ SNo_ (SNoLev x0) x0
Known SNoLev_ordinal^{SNoLev_ordinal} : ∀ x0 . SNo x0 ⟶ ordinal (SNoLev x0)
Theorem f4add.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ ∀ x2 x3 x4 . SNo x3 ⟶ x4 ∈ x3 ⟶ SetAdjoin x2 (Sing x0) = SetAdjoin x4 (Sing x1) ⟶ ∀ x5 : ο . x5 (proof)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 23602.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 . 68498.. x0 x1 ⟶ SNo x2 ⟶ 68498.. (ordsucc x0) (binunion x1 {SetAdjoin x3 (Sing x0)|x3 ∈ x2}) (proof)
Theorem a2c24.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 x3 x4 . 68498.. x0 x1 ⟶ binunion x1 {SetAdjoin x6 (Sing x0)|x6 ∈ x3} = binunion x2 {SetAdjoin x6 (Sing x0)|x6 ∈ x4} ⟶ x1 ⊆ x2 (proof)
Theorem 90357.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 x3 x4 . 68498.. x0 x1 ⟶ 68498.. x0 x2 ⟶ binunion x1 {SetAdjoin x6 (Sing x0)|x6 ∈ x3} = binunion x2 {SetAdjoin x6 (Sing x0)|x6 ∈ x4} ⟶ x1 = x2 (proof)
Theorem 3e83d.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 x3 x4 . 68498.. x0 x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ binunion x1 {SetAdjoin x6 (Sing x0)|x6 ∈ x3} = binunion x2 {SetAdjoin x6 (Sing x0)|x6 ∈ x4} ⟶ x3 ⊆ x4 (proof)
Theorem f57d5.. : ∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 x2 x3 x4 . 68498.. x0 x1 ⟶ 68498.. x0 x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ binunion x1 {SetAdjoin x6 (Sing x0)|x6 ∈ x3} = binunion x2 {SetAdjoin x6 (Sing x0)|x6 ∈ x4} ⟶ x3 = x4 (proof)
Theorem 42ea0.. : ∀ x0 x1 . SNo x0 ⟶ 68498.. x1 x0 (proof)
Theorem bfcc8.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ 68498.. 3 (ad280.. x0 x1) (proof)
Definition f4b0e.. := λ x0 x1 x2 x3 . binunion (binunion (binunion x0 {SetAdjoin x4 (Sing 2)|x4 ∈ x1}) {SetAdjoin x4 (Sing 3)|x4 ∈ x2}) {SetAdjoin x4 (Sing 4)|x4 ∈ x3}
Known nat_4^nat_4 : nat_p 4
Known In_1_4^In_1_4 : 1 ∈ 4
Known nat_3^nat_3 : nat_p 3
Known In_1_3^In_1_3 : 1 ∈ 3
Theorem 74b2d.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ 68498.. 5 (f4b0e.. x0 x1 x2 x3) (proof)
Theorem 84fad.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x0 = x4 (proof)
Theorem aa1e8.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x1 = x5 (proof)
Theorem 04ead.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x2 = x6 (proof)
Theorem 57cf4.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x3 = x7 (proof)
Definition 8c189.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (x0 = f4b0e.. x2 x4 x6 x8) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Theorem 70bda.. : ∀ x0 x1 x2 . f4b0e.. x0 x1 x2 0 = binunion (binunion x0 {SetAdjoin x4 (Sing 2)|x4 ∈ x1}) {SetAdjoin x4 (Sing 3)|x4 ∈ x2} (proof)
Theorem 27253.. : ∀ x0 x1 . f4b0e.. x0 x1 0 0 = ad280.. x0 x1 (proof)
Theorem fb499.. : ∀ x0 . f4b0e.. x0 0 0 0 = x0 (proof)
Theorem ca287.. : ∀ x0 . c7ce4.. x0 ⟶ 8c189.. x0 (proof)
Definition bbc71.. := λ x0 x1 x2 x3 x4 x5 x6 x7 . binunion (binunion (binunion (binunion (binunion (binunion (binunion x0 {SetAdjoin x8 (Sing 2)|x8 ∈ x1}) {SetAdjoin x8 (Sing 3)|x8 ∈ x2}) {SetAdjoin x8 (Sing 4)|x8 ∈ x3}) {SetAdjoin x8 (Sing 5)|x8 ∈ x4}) {SetAdjoin x8 (Sing 6)|x8 ∈ x5}) {SetAdjoin x8 (Sing 7)|x8 ∈ x6}) {SetAdjoin x8 (Sing 8)|x8 ∈ x7}
Known nat_8^nat_8 : nat_p 8
Known In_1_8^In_1_8 : 1 ∈ 8
Known nat_7^nat_7 : nat_p 7
Known In_1_7^In_1_7 : 1 ∈ 7
Known nat_6^nat_6 : nat_p 6
Known In_1_6^In_1_6 : 1 ∈ 6
Known nat_5^nat_5 : nat_p 5
Known In_1_5^In_1_5 : 1 ∈ 5
Theorem 0e211.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ 68498.. 9 (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) (proof)
Theorem cca09.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x0 = x8 (proof)
Theorem babe8.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x1 = x9 (proof)
Theorem 6488e.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x2 = x10 (proof)
Theorem ad01a.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x3 = x11 (proof)
Theorem f4559.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x4 = x12 (proof)
Theorem f56fc.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x5 = x13 (proof)
Theorem 4a66b.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x6 = x14 (proof)
Theorem 7c302.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x7 = x15 (proof)
Definition 1eb0a.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (∀ x15 : ο . (∀ x16 . and (SNo x16) (x0 = bbc71.. x2 x4 x6 x8 x10 x12 x14 x16) ⟶ x15) ⟶ x15) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Theorem b1d98.. : ∀ x0 x1 x2 x3 x4 x5 x6 . bbc71.. x0 x1 x2 x3 x4 x5 x6 0 = binunion (binunion (binunion (f4b0e.. x0 x1 x2 x3) {SetAdjoin x8 (Sing 5)|x8 ∈ x4}) {SetAdjoin x8 (Sing 6)|x8 ∈ x5}) {SetAdjoin x8 (Sing 7)|x8 ∈ x6} (proof)
Theorem 2e171.. : ∀ x0 x1 x2 x3 x4 x5 . bbc71.. x0 x1 x2 x3 x4 x5 0 0 = binunion (binunion (f4b0e.. x0 x1 x2 x3) {SetAdjoin x7 (Sing 5)|x7 ∈ x4}) {SetAdjoin x7 (Sing 6)|x7 ∈ x5} (proof)
Theorem 0fc47.. : ∀ x0 x1 x2 x3 x4 . bbc71.. x0 x1 x2 x3 x4 0 0 0 = binunion (f4b0e.. x0 x1 x2 x3) {SetAdjoin x6 (Sing 5)|x6 ∈ x4} (proof)
Theorem 3463c.. : ∀ x0 x1 x2 x3 . bbc71.. x0 x1 x2 x3 0 0 0 0 = f4b0e.. x0 x1 x2 x3 (proof)
Theorem b6032.. : ∀ x0 . 8c189.. x0 ⟶ 1eb0a.. x0 (proof)