Proofgold Address

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 : ι → ι
Param ordsucc^ordsucc : ι → ι
Known neq_0_2^neq_0_2 : 0 = 2 ⟶ ∀ x0 : ο . x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known In_0_2^In_0_2 : 0 ∈ 2
Theorem 325cb..^{not_TransSet_Sing2} : not (TransSet (Sing 2)) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition ordinal^ordinal := λ x0 . and (TransSet x0) (∀ x1 . x1 ∈ x0 ⟶ TransSet x1)
Theorem b9e15..^{not_ordinal_Sing2} : not (ordinal (Sing 2)) (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 ctagged_not_ordinal^{ctagged_not_ordinal} : ∀ x0 . not (ordinal (SetAdjoin x0 (Sing 2))) (proof)
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Theorem ctagged_notin_ordinal^{ctagged_notin_ordinal} : ∀ x0 x1 . ordinal x0 ⟶ nIn (SetAdjoin x1 (Sing 2)) x0 (proof)
Known neq_1_2^neq_1_2 : 1 = 2 ⟶ ∀ x0 : ο . x0
Theorem Sing2_notin_SingSing1^{Sing2_notin_SingSing1} : nIn (Sing 2) (Sing (Sing 1)) (proof)
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))
Definition SNo^SNo := λ x0 . ∀ x1 : ο . (∀ x2 . and (ordinal x2) (SNo_ x2 x0) ⟶ x1) ⟶ x1
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 ctagged_notin_SNo^{ctagged_notin_SNo} : ∀ x0 x1 . SNo x0 ⟶ nIn (SetAdjoin x1 (Sing 2)) x0 (proof)
Definition SNo_pair^SNo_pair := λ x0 x1 . binunion x0 {SetAdjoin x2 (Sing 2)|x2 ∈ x1}
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Theorem fca3d..^{SNo_pair_prop_1_Subq} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo_pair x0 x1 = SNo_pair x2 x3 ⟶ x0 ⊆ x2 (proof)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Theorem SNo_pair_prop_1^{SNo_pair_prop_1} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x2 ⟶ SNo_pair x0 x1 = SNo_pair x2 x3 ⟶ x0 = x2 (proof)
Theorem 9d654..^{ctagged_eqE_Subq} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SetAdjoin x2 (Sing 2) = SetAdjoin x3 (Sing 2) ⟶ x2 ⊆ x3 (proof)
Theorem ctagged_eqE_eq^{ctagged_eqE_eq} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SetAdjoin x2 (Sing 2) = SetAdjoin x3 (Sing 2) ⟶ x2 = x3 (proof)
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Theorem 25d53..^{SNo_pair_prop_2_Subq} : ∀ x0 x1 x2 x3 . SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo_pair x0 x1 = SNo_pair x2 x3 ⟶ x1 ⊆ x3 (proof)
Theorem SNo_pair_prop_2^{SNo_pair_prop_2} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo_pair x0 x1 = SNo_pair x2 x3 ⟶ x1 = x3 (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem SNo_pair_prop^{SNo_pair_prop} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo_pair x0 x1 = SNo_pair x2 x3 ⟶ and (x0 = x2) (x1 = x3) (proof)
Known Repl_Empty^Repl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0
Known binunion_idr^binunion_idr : ∀ x0 . binunion x0 0 = x0
Theorem SNo_pair_0^SNo_pair_0 : ∀ x0 . SNo_pair x0 0 = x0 (proof)
Definition CSNo^CSNo := λ x0 . ∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (x0 = SNo_pair x2 x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Theorem CSNo_I^CSNo_I : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ CSNo (SNo_pair x0 x1) (proof)
Theorem CSNo_E^CSNo_E : ∀ x0 . CSNo x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 . SNo x2 ⟶ SNo x3 ⟶ x0 = SNo_pair x2 x3 ⟶ x1 (SNo_pair x2 x3)) ⟶ x1 x0 (proof)
Known SNo_0^SNo_0 : SNo 0
Theorem SNo_CSNo^SNo_CSNo : ∀ x0 . SNo x0 ⟶ CSNo x0 (proof)
Definition Complex_i^Complex_i := SNo_pair 0 1
Known SNo_1^SNo_1 : SNo 1
Theorem SNo_Complex_i^{SNo_Complex_i} : CSNo Complex_i (proof)
Definition CSNo_Re^CSNo_Re := λ x0 . prim0 (λ x1 . and (SNo x1) (∀ x2 : ο . (∀ x3 . and (SNo x3) (x0 = SNo_pair x1 x3) ⟶ x2) ⟶ x2))
Definition CSNo_Im^CSNo_Im := λ x0 . prim0 (λ x1 . and (SNo x1) (x0 = SNo_pair (CSNo_Re x0) x1))
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem CSNo_Re1^CSNo_Re1 : ∀ x0 . CSNo x0 ⟶ and (SNo (CSNo_Re x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (x0 = SNo_pair (CSNo_Re x0) x2) ⟶ x1) ⟶ x1) (proof)
Theorem CSNo_Re2^CSNo_Re2 : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ CSNo_Re (SNo_pair x0 x1) = x0 (proof)
Theorem CSNo_Im1^CSNo_Im1 : ∀ x0 . CSNo x0 ⟶ and (SNo (CSNo_Im x0)) (x0 = SNo_pair (CSNo_Re x0) (CSNo_Im x0)) (proof)
Theorem CSNo_Im2^CSNo_Im2 : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ CSNo_Im (SNo_pair x0 x1) = x1 (proof)
Theorem CSNo_ReR^CSNo_ReR : ∀ x0 . CSNo x0 ⟶ SNo (CSNo_Re x0) (proof)
Theorem CSNo_ImR^CSNo_ImR : ∀ x0 . CSNo x0 ⟶ SNo (CSNo_Im x0) (proof)
Theorem CSNo_ReIm^CSNo_ReIm : ∀ x0 . CSNo x0 ⟶ x0 = SNo_pair (CSNo_Re x0) (CSNo_Im x0) (proof)
Theorem CSNo_ReIm_split^{CSNo_ReIm_split} : ∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ CSNo_Re x0 = CSNo_Re x1 ⟶ CSNo_Im x0 = CSNo_Im x1 ⟶ x0 = x1 (proof)
Param add_SNo^add_SNo : ι → ι → ι
Definition add_CSNo^add_CSNo := λ x0 x1 . SNo_pair (add_SNo (CSNo_Re x0) (CSNo_Re x1)) (add_SNo (CSNo_Im x0) (CSNo_Im x1))
Param mul_SNo^mul_SNo : ι → ι → ι
Param minus_SNo^minus_SNo : ι → ι
Definition mul_CSNo^mul_CSNo := λ x0 x1 . SNo_pair (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x1)) (minus_SNo (mul_SNo (CSNo_Im x0) (CSNo_Im x1)))) (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Im x1)) (mul_SNo (CSNo_Im x0) (CSNo_Re x1)))
Param ReplSep2^ReplSep2 : ι → (ι → ι) → (ι → ι → ο) → CT2 ι
Param Eps_i_realset : ι
Param True^True : ο
Definition f5776.. := ReplSep2 Eps_i_realset (λ x0 . Eps_i_realset) (λ x0 x1 . True) SNo_pair