Proofgold Address

Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Theorem 259b1.. : ∀ x0 . ∀ x1 x2 : ι → ι . prim5 (prim5 x0 x1) x2 = {x2 (x1 x4)|x4 ∈ x0} (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Known In_0_2^In_0_2 : 0 ∈ 2
Known In_1_2^In_1_2 : 1 ∈ 2
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Theorem e8716.. : ∀ x0 . atleastp u2 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x1) ⟶ x1 (proof)
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 u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Theorem 28d49.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u16 ⟶ x1 x2 ∈ u16) ⟶ ∀ x2 . x2 ⊆ u16 ⟶ prim5 x2 x1 ⊆ u16 (proof)
Param bij^bij : ι → ι → (ι → ι) → ο
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ 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 andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 43060.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u16 ⟶ ∀ x3 . x3 ∈ u16 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ ∀ x2 . x2 ⊆ u16 ⟶ equip x2 (prim5 x2 x1) (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 69049.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u16 ⟶ ∀ x3 . x3 ∈ u16 ⟶ x0 (x1 x2) (x1 x3) ⟶ x0 x2 x3) ⟶ ∀ x2 . x2 ⊆ u16 ⟶ (∀ 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 setminus^setminus : ι → ι → ι
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 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_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Known f6a92.. : 12 ∈ 13
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Known In_no3cycle^In_no3cycle : ∀ x0 x1 x2 . x0 ∈ x1 ⟶ x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ False
Known 3ef99.. : 13 ∈ 14
Known In_no4cycle^In_no4cycle : ∀ x0 x1 x2 x3 . x0 ∈ x1 ⟶ x1 ∈ x2 ⟶ x2 ∈ x3 ⟶ x3 ∈ x0 ⟶ False
Known 2e90c.. : 14 ∈ 15
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_16^nat_16 : nat_p 16
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 ea47f.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u16 ⟶ x1 x2 ∈ u16) ⟶ (∀ x2 . x2 ∈ u16 ⟶ ∀ x3 . x3 ∈ u16 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ (∀ x2 . x2 ∈ u16 ⟶ ∀ x3 . x3 ∈ u16 ⟶ x0 (x1 x2) (x1 x3) ⟶ x0 x2 x3) ⟶ (∀ x2 . x2 ∈ u16 ⟶ x1 (x1 (x1 (x1 x2))) = x2) ⟶ x1 u12 = u13 ⟶ x1 u13 = u14 ⟶ x1 u14 = u15 ⟶ x1 u15 = u12 ⟶ ∀ x2 . x2 ⊆ u16 ⟶ atleastp u6 x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x0 x3 x4)) ⟶ atleastp u2 (setminus x2 u12) ⟶ ∀ x3 : ο . (∀ x4 . x4 ⊆ u16 ⟶ atleastp u6 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u12 ∈ x4 ⟶ u13 ∈ x4 ⟶ x3) ⟶ (∀ x4 . x4 ⊆ u16 ⟶ atleastp u6 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u12 ∈ x4 ⟶ u14 ∈ x4 ⟶ x3) ⟶ x3 (proof)