a : Ordinal
⊢ ord (card (ord (succ (card a)))) = ord (succ (card a))
a : Ordinal
⊢ ord (succ (card a)) ∈ {b | ord (card b) = b}
dsimp
no goals
a : Ordinal
⊢ ord (card (ord (succ (card a)))) = ord (succ (card a))
rw [card_ord]