Proofgold Address

Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
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
Definition u12 := ordsucc u11
Definition Subq^Subq := λ x0 x1 . ∀ x2 . 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 4373b.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u12 ⟶ x1 x2 ∈ u12) ⟶ ∀ x2 . x2 ⊆ u12 ⟶ prim5 x2 x1 ⊆ u12 (proof)
Param bij^bij : ι → ι → (ι → ι) → ο
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known bijI^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ bij x0 x1 x2
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem afaa2.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u12 ⟶ ∀ x3 . x3 ∈ u12 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ ∀ x2 . x2 ⊆ u12 ⟶ equip x2 (prim5 x2 x1) (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 93347.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u12 ⟶ ∀ x3 . x3 ∈ u12 ⟶ x0 (x1 x2) (x1 x3) ⟶ x0 x2 x3) ⟶ ∀ x2 . x2 ⊆ u12 ⟶ (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x0 x3 x4)) ⟶ ∀ x3 . x3 ∈ prim5 x2 x1 ⟶ ∀ x4 . x4 ∈ prim5 x2 x1 ⟶ not (x0 x3 x4) (proof)
Param atleastp^atleastp : ι → ι → ο
Param setminus^setminus : ι → ι → ι
Known e8716.. : ∀ x0 . atleastp u2 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x1) ⟶ x1
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Known In_8_9^In_8_9 : 8 ∈ 9
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known In_no3cycle^In_no3cycle : ∀ x0 x1 x2 . x0 ∈ x1 ⟶ x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ False
Known fa1e6.. : 9 ∈ 10
Known In_no4cycle^In_no4cycle : ∀ x0 x1 x2 x3 . x0 ∈ x1 ⟶ x1 ∈ x2 ⟶ x2 ∈ x3 ⟶ x3 ∈ x0 ⟶ False
Known 9be62.. : 10 ∈ 11
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Param nat_p^nat_p : ι → ο
Param ordinal^ordinal : ι → ο
Known ordinal_trichotomy_or_impred^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (x0 ∈ x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (x1 ∈ x0 ⟶ x2) ⟶ x2
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known nat_p_trans^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Known nat_12^nat_12 : nat_p 12
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Theorem 7c829.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u12 ⟶ x1 x2 ∈ u12) ⟶ (∀ x2 . x2 ∈ u12 ⟶ ∀ x3 . x3 ∈ u12 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ (∀ x2 . x2 ∈ u12 ⟶ ∀ x3 . x3 ∈ u12 ⟶ x0 (x1 x2) (x1 x3) ⟶ x0 x2 x3) ⟶ x1 u9 = u8 ⟶ x1 u10 = u11 ⟶ x1 u11 = u9 ⟶ x0 u8 u11 ⟶ ∀ x2 . x2 ⊆ u12 ⟶ atleastp u5 x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x0 x3 x4)) ⟶ atleastp u2 (setminus x2 u8) ⟶ ∀ x3 : ο . (∀ x4 . x4 ⊆ u12 ⟶ atleastp u5 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u8 ∈ x4 ⟶ u9 ∈ x4 ⟶ x3) ⟶ (∀ x4 . x4 ⊆ u12 ⟶ atleastp u5 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u8 ∈ x4 ⟶ u10 ∈ x4 ⟶ x3) ⟶ (∀ x4 . x4 ⊆ u12 ⟶ atleastp u5 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u9 ∈ x4 ⟶ u10 ∈ x4 ⟶ x3) ⟶ x3 (proof)