Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ 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)
Param UPair^UPair : ι → ι → ι
Definition Sing^Sing := λ x0 . UPair x0 x0
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Theorem 8e626.. : ∀ x0 . Sing x0 = UPair x0 x0 (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem Sing_inv^Sing_inv : ∀ x0 x1 . Sing x0 = x1 ⟶ and (x0 ∈ x1) (∀ x2 . x2 ∈ x1 ⟶ x2 = x0) (proof)
Definition KPair_alt7 := λ x0 x1 . UPair (UPair x0 x1) (Sing x0)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Known UPairI1^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Known UPairI2^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Theorem 758c1.. : ∀ x0 x1 x2 x3 . KPair_alt7 x0 x1 = KPair_alt7 x2 x3 ⟶ x0 = x2 (proof)
Theorem f3ff4.. : ∀ x0 x1 x2 x3 . KPair_alt7 x0 x1 = KPair_alt7 x2 x3 ⟶ x1 = x3 (proof)
Theorem 40621.. : ∀ x0 x1 x2 x3 . KPair_alt7 x0 x1 = KPair_alt7 x2 x3 ⟶ and (x0 = x2) (x1 = x3) (proof)
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Definition ccad8.. := λ x0 x1 . ∀ x2 : ο . (∀ x3 . and (and (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x1) (KPair_alt7 x4 x6 ∈ x3) ⟶ x5) ⟶ x5) (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (KPair_alt7 x6 x4 ∈ x3) ⟶ x5) ⟶ x5)) (∀ x4 x5 x6 x7 . KPair_alt7 x4 x5 ∈ x3 ⟶ KPair_alt7 x6 x7 ∈ x3 ⟶ iff (x4 = x6) (x5 = x7)) ⟶ x2) ⟶ x2
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem a138b.. : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ ccad8.. x0 x1 (proof)
Known Eps_i_ax^Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Theorem 536c8.. : ∀ x0 x1 . ccad8.. x0 x1 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2 (proof)
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem and5I^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4 (proof)
Known and4E^and4E : ∀ x0 x1 x2 x3 : ο . and (and (and x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4) ⟶ x4
Theorem and5E^and5E : ∀ x0 x1 x2 x3 x4 : ο . and (and (and (and x0 x1) x2) x3) x4 ⟶ ∀ x5 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5) ⟶ x5 (proof)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known or4I1^or4I1 : ∀ x0 x1 x2 x3 : ο . x0 ⟶ or (or (or x0 x1) x2) x3
Theorem or5I1^or5I1 : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Known or4I2^or4I2 : ∀ x0 x1 x2 x3 : ο . x1 ⟶ or (or (or x0 x1) x2) x3
Theorem or5I2^or5I2 : ∀ x0 x1 x2 x3 x4 : ο . x1 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Known or4I3^or4I3 : ∀ x0 x1 x2 x3 : ο . x2 ⟶ or (or (or x0 x1) x2) x3
Theorem or5I3^or5I3 : ∀ x0 x1 x2 x3 x4 : ο . x2 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Known or4I4^or4I4 : ∀ x0 x1 x2 x3 : ο . x3 ⟶ or (or (or x0 x1) x2) x3
Theorem or5I4^or5I4 : ∀ x0 x1 x2 x3 x4 : ο . x3 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem or5I5^or5I5 : ∀ x0 x1 x2 x3 x4 : ο . x4 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Known or4E^or4E : ∀ x0 x1 x2 x3 : ο . or (or (or x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x4) ⟶ (x1 ⟶ x4) ⟶ (x2 ⟶ x4) ⟶ (x3 ⟶ x4) ⟶ x4
Theorem or5E^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 (proof)
Theorem and6I^and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ and (and (and (and (and x0 x1) x2) x3) x4) x5 (proof)
Theorem and6E^and6E : ∀ x0 x1 x2 x3 x4 x5 : ο . and (and (and (and (and x0 x1) x2) x3) x4) x5 ⟶ ∀ x6 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6) ⟶ x6 (proof)
Theorem and7I^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 (proof)
Theorem and7E^and7E : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6 ⟶ ∀ x7 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7) ⟶ x7 (proof)