Metamath Proof Explorer


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 ℵ )