We will prove S_Omega ∉ R.
Assume HS: S_Omega ∈ R.
Apply FalseE to the current goal.
We prove the intermediate claim HRdef: R = real.
Use reflexivity.
We prove the intermediate claim HSreal: S_Omega ∈ real.
An exact proof term for the current goal is (mem_eqR S_Omega R real HRdef HS).
We prove the intermediate claim HSbase: S_Omega ∈ SNoS_ (ordsucc ω).
Apply (real_E S_Omega HSreal (S_Omega ∈ SNoS_ (ordsucc ω))) to the current goal.
Assume HSNo HSLev HSsnoS Hlow Hhigh Huniq Hrat.
An exact proof term for the current goal is HSsnoS.
We prove the intermediate claim HSwo: well_ordered_set S_Omega.
An exact proof term for the current goal is (andEL (well_ordered_set S_Omega) (uncountable_set S_Omega) S_Omega_well_ordered_uncountable).
We prove the intermediate claim HSord: ordinal S_Omega.
An exact proof term for the current goal is (well_ordered_set_is_ordinal S_Omega HSwo).
We prove the intermediate claim HalphaOrd: ordinal (ordsucc ω).
An exact proof term for the current goal is ordsucc_omega_ordinal.
Apply (SNoS_E (ordsucc ω) HalphaOrd S_Omega HSbase) to the current goal.
Let beta be given.
Assume Hbeta: beta ∈ ordsucc ω ∧ SNo_ beta S_Omega.
We prove the intermediate claim HbetaIn: beta ∈ ordsucc ω.
An exact proof term for the current goal is (andEL (beta ∈ ordsucc ω) (SNo_ beta S_Omega) Hbeta).
We prove the intermediate claim HSno_beta: SNo_ beta S_Omega.
An exact proof term for the current goal is (andER (beta ∈ ordsucc ω) (SNo_ beta S_Omega) Hbeta).
We prove the intermediate claim HSno_self: SNo_ S_Omega S_Omega.
An exact proof term for the current goal is (ordinal_SNo_ S_Omega HSord).
We prove the intermediate claim Heq: beta = S_Omega.
An exact proof term for the current goal is (SNoLev_uniq S_Omega beta S_Omega (ordinal_Hered (ordsucc ω) HalphaOrd beta HbetaIn) HSord HSno_beta HSno_self).
We prove the intermediate claim HS_in_ordsucc_omega: S_Omega ∈ ordsucc ω.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HbetaIn.
We prove the intermediate claim Hunc: uncountable_set S_Omega.
An exact proof term for the current goal is (andER (well_ordered_set S_Omega) (uncountable_set S_Omega) S_Omega_well_ordered_uncountable).
We prove the intermediate claim Hcount: countable_set S_Omega.
We prove the intermediate claim Hor: S_Omega ∈ ω ∨ S_Omega = ω.
An exact proof term for the current goal is (ordsuccE ω S_Omega HS_in_ordsucc_omega).
Apply (Hor (countable_set S_Omega)) to the current goal.
Assume HSomega: S_Omega ∈ ω.
We prove the intermediate claim Hsub: S_Omega ⊆ ω.
An exact proof term for the current goal is (omega_TransSet S_Omega HSomega).
We prove the intermediate claim HomegaCount: countable ω.
An exact proof term for the current goal is omega_countable_set.
We will prove countable_set S_Omega.
An exact proof term for the current goal is (Subq_countable S_Omega ω HomegaCount Hsub).
Assume Heqomega: S_Omega = ω.
rewrite the current goal using Heqomega (from left to right).
An exact proof term for the current goal is omega_countable_set.
An exact proof term for the current goal is (Hunc Hcount).
∎