Theory "ucord"

Signature

Definitions

omega1_def

⊢ ω₁ = sup {a | countableOrd a}

Theorems

x_lt_omega1_countable

⊢ x < ω₁ ⇔ countableOrd x

Unum_cardlt_ucinf

⊢ 𝕌(:num) ≺ 𝕌(:num + α + (num -> bool))

Unum_cardle_ucinf

⊢ 𝕌(:num) ≼ 𝕌(:num + α + (num -> bool))

ucord_sup_exists_lemma

⊢ {a | countableOrd a} ≼ 𝕌(:num + α + (num -> bool))

ucinf_uncountable

⊢ ¬COUNTABLE 𝕌(:num + α + (num -> bool))

omega1_not_countable

⊢ ¬countableOrd ω₁