Proofgold Address

Param bij^bij : ι → ι → (ι → ι) → ο
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Param real^real : ι
Param omega^omega : ι
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
Known 2c48a..^{atleastp_antisym_equip} : ∀ x0 x1 . atleastp x0 x1 ⟶ atleastp x1 x0 ⟶ equip x0 x1
Param SNoS_^SNoS_ : ι → ι
Param ordsucc^ordsucc : ι → ι
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known Subq_atleastp^{Subq_atleastp} : ∀ x0 x1 . x0 ⊆ x1 ⟶ atleastp x0 x1
Param SNo^SNo : ι → ο
Param SNoLev^SNoLev : ι → ι
Param SNoLt^SNoLt : ι → ι → ο
Param minus_SNo^minus_SNo : ι → ι
Param abs_SNo^abs_SNo : ι → ι
Param add_SNo^add_SNo : ι → ι → ι
Param eps_^eps_ : ι → ι
Known real_E^real_E : ∀ x0 . x0 ∈ real ⟶ ∀ x1 : ο . (SNo x0 ⟶ SNoLev x0 ∈ ordsucc omega ⟶ x0 ∈ SNoS_ (ordsucc omega) ⟶ SNoLt (minus_SNo omega) x0 ⟶ SNoLt x0 omega ⟶ (∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3)) ⟶ x2 = x0) ⟶ (∀ x2 . x2 ∈ omega ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ SNoS_ omega) (and (SNoLt x4 x0) (SNoLt x0 (add_SNo x4 (eps_ x2)))) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Definition ordinal^ordinal := λ x0 . and (TransSet x0) (∀ x1 . x1 ∈ x0 ⟶ TransSet x1)
Param binunion^binunion : ι → ι → ι
Param SetAdjoin^SetAdjoin : ι → ι → ι
Param Sing^Sing : ι → ι
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))
Known SNoS_I^SNoS_I : ∀ x0 . ordinal x0 ⟶ ∀ x1 x2 . x2 ∈ x0 ⟶ SNo_ x2 x1 ⟶ x1 ∈ SNoS_ x0
Known ordsucc_omega_ordinal^{ordsucc_omega_ordinal} : ordinal (ordsucc omega)
Known SNoLev_^SNoLev_ : ∀ x0 . SNo x0 ⟶ SNo_ (SNoLev x0) x0
Known atleastp_SNoS_ordsucc_omega_Power_omega^{atleastp_SNoS_ordsucc_omega_Power_omega} : atleastp (SNoS_ (ordsucc omega)) (prim4 omega)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Param If_i^If_i : ο → ι → ι → ι
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Param nat_p^nat_p : ι → ο
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Param finite^finite : ι → ο
Param SNoLe^SNoLe : ι → ι → ο
Definition SNo_max_of^SNo_max_of := λ x0 x1 . and (and (x1 ∈ x0) (SNo x1)) (∀ x2 . x2 ∈ x0 ⟶ SNo x2 ⟶ SNoLe x2 x1)
Definition SNo_min_of^SNo_min_of := λ x0 x1 . and (and (x1 ∈ x0) (SNo x1)) (∀ x2 . x2 ∈ x0 ⟶ SNo x2 ⟶ SNoLe x1 x2)
Param famunion^famunion : ι → (ι → ι) → ι
Definition SNoCutP^SNoCutP := λ x0 x1 . and (and (∀ x2 . x2 ∈ x0 ⟶ SNo x2) (∀ x2 . x2 ∈ x1 ⟶ SNo x2)) (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3)
Param SNoCut^SNoCut : ι → ι → ι
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Param ReplSep^ReplSep : ι → (ι → ο) → (ι → ι) → ι
Param setminus^setminus : ι → ι → ι
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known real_add_SNo^real_add_SNo : ∀ x0 . x0 ∈ real ⟶ ∀ x1 . x1 ∈ real ⟶ add_SNo x0 x1 ∈ real
Known SNoS_omega_real^{SNoS_omega_real} : SNoS_ omega ⊆ real
Known omega_SNoS_omega^{omega_SNoS_omega} : omega ⊆ SNoS_ omega
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_1^nat_1 : nat_p 1
Definition infinite^infinite := λ x0 . not (finite x0)
Known real_minus_SNo^{real_minus_SNo} : ∀ x0 . x0 ∈ real ⟶ minus_SNo x0 ∈ real
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Known real_SNoCut_SNoS_omega^{real_SNoCut_SNoS_omega} : ∀ x0 . x0 ⊆ SNoS_ omega ⟶ ∀ x1 . x1 ⊆ SNoS_ omega ⟶ SNoCutP x0 x1 ⟶ (x0 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (x1 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (SNoLt x2 x4) ⟶ x3) ⟶ x3) ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (SNoLt x4 x2) ⟶ x3) ⟶ x3) ⟶ SNoCut x0 x1 ∈ real
Known famunionE_impred^{famunionE_impred} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 ∈ x1 x4 ⟶ x3) ⟶ x3
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known omega_ordinal^{omega_ordinal} : ordinal omega
Known nat_0^nat_0 : nat_p 0
Known ordinal_SNo_^ordinal_SNo_ : ∀ x0 . ordinal x0 ⟶ SNo_ x0 x0
Known ordinal_Empty^{ordinal_Empty} : ordinal 0
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known add_SNo_SNoS_omega^{add_SNo_SNoS_omega} : ∀ x0 . x0 ∈ SNoS_ omega ⟶ ∀ x1 . x1 ∈ SNoS_ omega ⟶ add_SNo x0 x1 ∈ SNoS_ omega
Known SNo_eps_SNoS_omega^{SNo_eps_SNoS_omega} : ∀ x0 . x0 ∈ omega ⟶ eps_ x0 ∈ SNoS_ omega
Known omega_ordsucc^{omega_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ ordsucc x0 ∈ omega
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known minus_SNo_SNoS_omega^{minus_SNo_SNoS_omega} : ∀ x0 . x0 ∈ SNoS_ omega ⟶ minus_SNo x0 ∈ SNoS_ omega
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known infinite_bigger^{infinite_bigger} : ∀ x0 . x0 ⊆ omega ⟶ infinite x0 ⟶ ∀ x1 . x1 ∈ omega ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (x1 ∈ x3) ⟶ x2) ⟶ x2
Known famunionI^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ x0 ⟶ x3 ∈ x1 x2 ⟶ x3 ∈ famunion x0 x1
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known add_SNo_eps_Lt^{add_SNo_eps_Lt} : ∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ omega ⟶ SNoLt x0 (add_SNo x0 (eps_ x1))
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known add_SNo_0R^add_SNo_0R : ∀ x0 . SNo x0 ⟶ add_SNo x0 0 = x0
Known add_SNo_Lt2^add_SNo_Lt2 : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x1 x2 ⟶ SNoLt (add_SNo x0 x1) (add_SNo x0 x2)
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Known SNo_eps_^SNo_eps_ : ∀ x0 . x0 ∈ omega ⟶ SNo (eps_ x0)
Known SNo_0^SNo_0 : SNo 0
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Known minus_SNo_Lt_contra^{minus_SNo_Lt_contra} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLt x0 x1 ⟶ SNoLt (minus_SNo x1) (minus_SNo x0)
Known SNo_eps_pos^SNo_eps_pos : ∀ x0 . x0 ∈ omega ⟶ SNoLt 0 (eps_ x0)
Known PowerE^PowerE : ∀ x0 x1 . x1 ∈ prim4 x0 ⟶ x1 ⊆ x0
Known SNoS_E2^SNoS_E2 : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ ∀ x2 : ο . (SNoLev x1 ∈ x0 ⟶ ordinal (SNoLev x1) ⟶ SNo x1 ⟶ SNo_ (SNoLev x1) x1 ⟶ x2) ⟶ x2
Known add_SNo_cancel_R^{add_SNo_cancel_R} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 x1 = add_SNo x2 x1 ⟶ x0 = x2
Known SNo_1^SNo_1 : SNo 1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known SNoLt_irref^SNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known SNoLt_tra^SNoLt_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x1 ⟶ SNoLt x1 x2 ⟶ SNoLt x0 x2
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known SNo_add_SNo^SNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
Known SNoLt_0_1^SNoLt_0_1 : SNoLt 0 1
Known minus_SNo_Lt_contra1^{minus_SNo_Lt_contra1} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLt (minus_SNo x0) x1 ⟶ SNoLt (minus_SNo x1) x0
Known add_SNo_0L^add_SNo_0L : ∀ x0 . SNo x0 ⟶ add_SNo 0 x0 = x0
Known add_SNo_Lt1^add_SNo_Lt1 : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x2 ⟶ SNoLt (add_SNo x0 x1) (add_SNo x2 x1)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known minus_SNo_invol^{minus_SNo_invol} : ∀ x0 . SNo x0 ⟶ minus_SNo (minus_SNo x0) = x0
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known ReplSepE_impred^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ ReplSep x0 x1 x2 ⟶ ∀ x4 : ο . (∀ x5 . x5 ∈ x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Known tagged_not_ordinal^{tagged_not_ordinal} : ∀ x0 . not (ordinal (SetAdjoin x0 (Sing 1)))
Definition PNoEq_^PNoEq_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 . x3 ∈ x0 ⟶ iff (x1 x3) (x2 x3)
Definition SNoEq_^SNoEq_ := λ x0 x1 x2 . PNoEq_ x0 (λ x3 . x3 ∈ x1) (λ x3 . x3 ∈ x2)
Known SNoLtI2^SNoLtI2 : ∀ x0 x1 . SNoLev x0 ∈ SNoLev x1 ⟶ SNoEq_ (SNoLev x0) x0 x1 ⟶ SNoLev x0 ∈ x1 ⟶ SNoLt x0 x1
Known SNoLev_0^SNoLev_0 : SNoLev 0 = 0
Known least_ordinal_ex^{least_ordinal_ex} : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2) ⟶ x1) ⟶ x1) ⟶ ∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . x3 ∈ x2 ⟶ not (x0 x3)) ⟶ x1) ⟶ x1
Known SNo_SNo^SNo_SNo : ∀ x0 . ordinal x0 ⟶ ∀ x1 . SNo_ x0 x1 ⟶ SNo x1
Known famunion_Empty^{famunion_Empty} : ∀ x0 : ι → ι . famunion 0 x0 = 0
Known binunion_idl^binunion_idl : ∀ x0 . binunion 0 x0 = x0
Known finite_max_exists^{finite_max_exists} : ∀ x0 . (∀ x1 . x1 ∈ x0 ⟶ SNo x1) ⟶ finite x0 ⟶ (x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ ∀ x1 : ο . (∀ x2 . SNo_max_of x0 x2 ⟶ x1) ⟶ x1
Known nat_p_SNo^nat_p_SNo : ∀ x0 . nat_p x0 ⟶ SNo x0
Known ordinal_In_Or_Subq^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ∈ x1) (x1 ⊆ x0)
Known SNoLeLt_tra^SNoLeLt_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x1 ⟶ SNoLt x1 x2 ⟶ SNoLt x0 x2
Known SNoLtLe_tra^SNoLtLe_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x1 ⟶ SNoLe x1 x2 ⟶ SNoLt x0 x2
Known ordinal_SNo^ordinal_SNo : ∀ x0 . ordinal x0 ⟶ SNo x0
Known ordinal_In_SNoLt^{ordinal_In_SNoLt} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ SNoLt x1 x0
Known ordinal_Subq_SNoLe^{ordinal_Subq_SNoLe} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ x0 ⊆ x1 ⟶ SNoLe x0 x1
Known ordinal_Hered^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordinal x1
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known exactly1of2_I2^{exactly1of2_I2} : ∀ x0 x1 : ο . not x0 ⟶ x1 ⟶ exactly1of2 x0 x1
Known tagged_eqE_eq^{tagged_eqE_eq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ SetAdjoin x0 (Sing 1) = SetAdjoin x1 (Sing 1) ⟶ x0 = x1
Known exactly1of2_I1^{exactly1of2_I1} : ∀ x0 x1 : ο . x0 ⟶ not x1 ⟶ exactly1of2 x0 x1
Known ReplSepI^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⟶ x2 x3 ∈ ReplSep x0 x1 x2
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 binunion_finite^{binunion_finite} : ∀ x0 . finite x0 ⟶ ∀ x1 . finite x1 ⟶ finite (binunion x0 x1)
Known 28148..^Sing_finite : ∀ x0 . finite (Sing x0)
Known Repl_finite^Repl_finite : ∀ x0 : ι → ι . ∀ x1 . finite x1 ⟶ finite (prim5 x1 x0)
Known neq_ordsucc_0^{neq_ordsucc_0} : ∀ x0 . ordsucc x0 = 0 ⟶ ∀ x1 : ο . x1
Known ordsucc_inj^ordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1 ⟶ x0 = x1
Known SNoCutP_SNoCut_impred^{SNoCutP_SNoCut_impred} : ∀ x0 x1 . SNoCutP x0 x1 ⟶ ∀ x2 : ο . (SNo (SNoCut x0 x1) ⟶ SNoLev (SNoCut x0 x1) ∈ ordsucc (binunion (famunion x0 (λ x3 . ordsucc (SNoLev x3))) (famunion x1 (λ x3 . ordsucc (SNoLev x3)))) ⟶ (∀ x3 . x3 ∈ x0 ⟶ SNoLt x3 (SNoCut x0 x1)) ⟶ (∀ x3 . x3 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x3) ⟶ (∀ x3 . SNo x3 ⟶ (∀ x4 . x4 ∈ x0 ⟶ SNoLt x4 x3) ⟶ (∀ x4 . x4 ∈ x1 ⟶ SNoLt x3 x4) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x3) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x3)) ⟶ x2) ⟶ x2
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Known finite_min_exists^{finite_min_exists} : ∀ x0 . (∀ x1 . x1 ∈ x0 ⟶ SNo x1) ⟶ finite x0 ⟶ (x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ ∀ x1 : ο . (∀ x2 . SNo_min_of x0 x2 ⟶ x1) ⟶ x1
Known eps_ordsucc_half_add^{eps_ordsucc_half_add} : ∀ x0 . nat_p x0 ⟶ add_SNo (eps_ (ordsucc x0)) (eps_ (ordsucc x0)) = eps_ x0
Known add_SNo_assoc^{add_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Known add_SNo_minus_R2^{add_SNo_minus_R2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo (add_SNo x0 x1) (minus_SNo x1) = x0
Known eps_0_1^eps_0_1 : eps_ 0 = 1
Known SNoLe_antisym^{SNoLe_antisym} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe x0 x1 ⟶ SNoLe x1 x0 ⟶ x0 = x1
Known add_SNo_Le1^add_SNo_Le1 : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x2 ⟶ SNoLe (add_SNo x0 x1) (add_SNo x2 x1)
Known nat_inv_impred^{nat_inv_impred} : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known nat_0_in_ordsucc^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Known binunion_Subq_1^{binunion_Subq_1} : ∀ x0 x1 . x0 ⊆ binunion x0 x1
Theorem equip_real_Power_omega^{equip_real_Power_omega} : equip real (prim4 omega) (proof)
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known form100_22_v2^{form100_22_v2} : ∀ x0 : ι → ι . not (inj (prim4 omega) omega x0)
Known inj_comp^inj_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . inj x0 x1 x3 ⟶ inj x1 x2 x4 ⟶ inj x0 x2 (λ x5 . x4 (x3 x5))
Known bij_inj^bij_inj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ inj x0 x1 x2
Theorem form100_22_real_uncountable_atleastp^{form100_22_real_uncountable_atleastp} : not (atleastp real omega) (proof)
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Theorem form100_22_real_uncountable_equip^{form100_22_real_uncountable_equip} : not (equip real omega) (proof)