Theory "ucord"

Signature

Definitions

omega1_def

⊢ ω₁ = sup {a | countableOrd a}

Theorems

ucinf_uncountable

⊢ ¬countable 𝕌(:α ucinf)

Unum_cardlt_ucinf

⊢ 𝕌(:num) <

Unum_cardle_ucinf

⊢ 𝕌(:num) ≼ 𝕌(:α ucinf)


ucord_sup_exists_lemma

⊢ {a | countableOrd a} ≼ 𝕌(:α ucinf)


x_lt_omega1_countable

⊢ x < ω₁ ⇔ countableOrd x


omega1_not_countable

⊢ ¬countableOrd ω₁