This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Infinity Cardinal numbers 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
eqabi ⊢ ( ω ∪ ran ℵ ) = { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 }
4
3
eqcomi ⊢ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } = ( ω ∪ ran ℵ )