Theorem cardnum

Description: Two ways to express the class of all cardinal numbers, which consists of the finite ordinals in _om plus the transfinite alephs. (Contributed by NM, 10-Sep-2004)

	Ref	Expression
Assertion	cardnum	⊢ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } = ( ω ∪ ran ℵ )

Proof

Step	Hyp	Ref	Expression
1		iscard3	⊢ ( ( card ‘ 𝑥 ) = 𝑥 ↔ 𝑥 ∈ ( ω ∪ ran ℵ ) )
2	1	bicomi	⊢ ( 𝑥 ∈ ( ω ∪ ran ℵ ) ↔ ( card ‘ 𝑥 ) = 𝑥 )
3	2	abbi2i	⊢ ( ω ∪ ran ℵ ) = { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 }
4	3	eqcomi	⊢ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } = ( ω ∪ ran ℵ )