o : Ordinal
ho : Ordinal.IsLimit o
a : Ordinal
ha : ∀ (b : Ordinal), b < o → ord (beth b) ≤ a
⊢ (⨆ (a : ↑(Iio o)), beth ↑a) ≤ card a
o : Ordinal
ho : Ordinal.IsLimit o
a : Ordinal
ha : ∀ (b : Ordinal), b < o → ord (beth b) ≤ a
⊢ ord (beth o) ≤ a
rw [beth_limit ho, ord_le]
no goals
o : Ordinal
ho : Ordinal.IsLimit o
a : Ordinal
ha : ∀ (b : Ordinal), b < o → ord (beth b) ≤ a
⊢ (⨆ (a : ↑(Iio o)), beth ↑a) ≤ card a
exact ciSup_le' fun b => ord_le.1 (ha _ b.2)