c : Cardinal
hc : ℵ₀ ≤ c
a b : Ordinal
ha : card a < c
hb : card b < c
⊢ card a + card b < c
c : Cardinal
hc : ℵ₀ ≤ c
a b : Ordinal
ha : a < ord c
hb : b < ord c
⊢ (fun x x_1 => x + x_1) a b < ord c
rw [lt_ord, Ordinal.card_add] at *
no goals
c : Cardinal
hc : ℵ₀ ≤ c
a b : Ordinal
ha : card a < c
hb : card b < c
⊢ card a + card b < c
exact add_lt_of_lt hc ha hb