Proofgold Address

Param nat_p^nat_p : ι → ο
Param equip^equip : ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Param ordinal^ordinal : ι → ο
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param binunion^binunion : ι → ι → ι
Param Sing^Sing : ι → ι
Param atleastp^atleastp : ι → ι → ο
Known 2ec5a.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . atleastp (ordsucc x0) x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ordinal x2) ⟶ ∀ x2 : ο . (∀ x3 x4 . equip x0 x3 ⟶ x4 ∈ x1 ⟶ x3 ⊆ x1 ⟶ x3 ⊆ x4 ⟶ x2) ⟶ x2
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param omega^omega : ι
Definition finite^finite := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (equip x0 x2) ⟶ x1) ⟶ x1
Known 1b508.. : ∀ x0 x1 . finite x0 ⟶ atleastp x1 x0 ⟶ x0 ⊆ x1 ⟶ x0 = x1
Known adjoin_finite^{adjoin_finite} : ∀ x0 x1 . finite x0 ⟶ finite (binunion x0 (Sing x1))
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Param add_nat^add_nat : ι → ι → ι
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_0^nat_0 : nat_p 0
Param setsum^setsum : ι → ι → ι
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0 ⟶ nat_p x1 ⟶ equip x0 x2 ⟶ equip x1 x3 ⟶ equip (add_nat x0 x1) (setsum x2 x3)
Known nat_1^nat_1 : nat_p 1
Known equip_ref^equip_ref : ∀ x0 . equip x0 x0
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known d778e.. : ∀ x0 x1 x2 x3 . equip x0 x2 ⟶ equip x1 x3 ⟶ (∀ x4 . x4 ∈ x0 ⟶ nIn x4 x1) ⟶ equip (binunion x0 x1) (setsum x2 x3)
Definition u1 := 1
Known 5169f..^equip_Sing_1 : ∀ x0 . equip (Sing x0) u1
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Theorem be1cd.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . equip (ordsucc x0) x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ordinal x2) ⟶ ∀ x2 : ο . (∀ x3 x4 . equip x0 x3 ⟶ x4 ∈ x1 ⟶ x3 ⊆ x1 ⟶ x3 ⊆ x4 ⟶ x1 = binunion x3 (Sing x4) ⟶ x2) ⟶ x2 (proof)
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Theorem 480b2.. : add_nat u3 u1 = u4 (proof)
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Param u13 : ι
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known nat_17^nat_17 : nat_p u17
Known e57ea.. : u11 ∈ u17
Theorem b4ae4.. : u11 ⊆ u17 (proof)
Known nat_8^nat_8 : nat_p 8
Known In_6_8^In_6_8 : 6 ∈ 8
Theorem bd770.. : u6 ⊆ u8 (proof)
Known In_7_8^In_7_8 : 7 ∈ 8
Theorem 021ac.. : u7 ⊆ u8 (proof)
Param setminus^setminus : ι → ι → ι
Definition u12 := ordsucc u11
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known 660da.. : ∀ x0 . x0 ∈ u16 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 46814.. : 0 ∈ 12
Known 2b77d.. : 1 ∈ 12
Known 7c2ac.. : 2 ∈ 12
Known 2f583.. : 3 ∈ 12
Known e4fc0.. : 4 ∈ 12
Known 04716.. : 5 ∈ 12
Known fbe39.. : 6 ∈ 12
Known 35d73.. : 7 ∈ 12
Known 5196c.. : 8 ∈ 12
Known 4fa36.. : 9 ∈ 12
Known 42552.. : 10 ∈ 12
Known fee2e.. : 11 ∈ 12
Theorem ee881.. : ∀ x0 . x0 ∈ setminus u16 u12 ⟶ ∀ x1 : ι → ο . x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 x0 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Theorem 4fd0a.. : ∀ x0 . x0 ∈ setminus u17 u12 ⟶ ∀ x1 : ι → ο . x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 x0 (proof)
Definition u18 := ordsucc u17
Theorem 7618f.. : ∀ x0 . x0 ∈ setminus u18 u12 ⟶ ∀ x1 : ι → ο . x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 x0 (proof)
Known 866c8.. : ∀ x0 . x0 ∈ u12 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 x0
Known In_0_6^In_0_6 : 0 ∈ 6
Known In_1_6^In_1_6 : 1 ∈ 6
Known In_2_6^In_2_6 : 2 ∈ 6
Known In_3_6^In_3_6 : 3 ∈ 6
Known In_4_6^In_4_6 : 4 ∈ 6
Known In_5_6^In_5_6 : 5 ∈ 6
Theorem 49949.. : ∀ x0 . x0 ∈ setminus u12 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 x0 (proof)
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Theorem 823c9.. : ∀ x0 . x0 ∈ setminus u16 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 x0 (proof)
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Theorem 0420f.. : ∀ x0 . x0 ∈ setminus u15 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 x0 (proof)
Theorem a1137.. : ∀ x0 . x0 ∈ setminus u14 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 x0 (proof)
Theorem 5786d.. : ∀ x0 . x0 ∈ setminus u13 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 x0 (proof)
Theorem 090fa.. : ∀ x0 . x0 ∈ setminus u11 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 x0 (proof)
Theorem 86222.. : ∀ x0 . x0 ∈ setminus u10 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 x0 (proof)
Theorem 27661.. : ∀ x0 . x0 ∈ setminus u12 u10 ⟶ ∀ x1 : ι → ο . x1 u10 ⟶ x1 u11 ⟶ x1 x0 (proof)
Theorem 853d4.. : ∀ x0 . x0 ∈ setminus u16 u10 ⟶ ∀ x1 : ι → ο . x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 x0 (proof)
Theorem 332b1.. : ∀ x0 . x0 ∈ setminus u15 u10 ⟶ ∀ x1 : ι → ο . x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 x0 (proof)
Theorem 98cac.. : ∀ x0 . x0 ∈ setminus u14 u10 ⟶ ∀ x1 : ι → ο . x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 x0 (proof)
Theorem fc2d4.. : ∀ x0 . x0 ∈ setminus u13 u10 ⟶ ∀ x1 : ι → ο . x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 x0 (proof)
Known In_0_8^In_0_8 : 0 ∈ 8
Known In_1_8^In_1_8 : 1 ∈ 8
Known In_2_8^In_2_8 : 2 ∈ 8
Known In_3_8^In_3_8 : 3 ∈ 8
Known In_4_8^In_4_8 : 4 ∈ 8
Known In_5_8^In_5_8 : 5 ∈ 8
Theorem bf41f.. : ∀ x0 . x0 ∈ setminus u12 u8 ⟶ ∀ x1 : ι → ο . x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 x0 (proof)