case intro
o : Ordinal
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal
ha : ord (aleph' a) = o
⊢ ∃ a, ord (aleph a) = o
o : Ordinal
ho : ord (card o) = o
ho' : ω ≤ o
⊢ ∃ a, ord (aleph a) = o
cases' eq_aleph'_of_eq_card_ord ho with a ha
case intro
o : Ordinal
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal
ha : ord (aleph' a) = o
⊢ ord (aleph (a - ω)) = o
case intro
o : Ordinal
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal
ha : ord (aleph' a) = o
⊢ ∃ a, ord (aleph a) = o
use a - ω
case intro
o : Ordinal
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal
ha : ord (aleph' a) = o
⊢ ord (aleph' (ω + (a - ω))) = o
case intro
o : Ordinal
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal
ha : ord (aleph' a) = o
⊢ ord (aleph (a - ω)) = o
unfold aleph
case intro
o : Ordinal
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal
ha : ord (aleph' a) = o
⊢ ω ≤ a
case intro
o : Ordinal
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal
ha : ord (aleph' a) = o
⊢ ord (aleph' (ω + (a - ω))) = o
rwa [Ordinal.add_sub_cancel_of_le]
no goals
case intro
o : Ordinal
ho : ord (card o) = o
ho' : ω ≤ o
a : Ordinal
ha : ord (aleph' a) = o
⊢ ω ≤ a
rwa [← aleph0_le_aleph', ← ord_le_ord, ha, ord_aleph0]