This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscard3

Description: Two ways to express the property of being a cardinal number. (Contributed by NM, 9-Nov-2003)

Ref Expression
Assertion iscard3 ( ( card ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ ( ω ∪ ran ℵ ) )

Proof

Step Hyp Ref Expression
1 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
2 eleq1 ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ( card ‘ 𝐴 ) ∈ On ↔ 𝐴 ∈ On ) )
3 1 2 mpbii ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ On )
4 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
5 3 4 syl ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → Ord 𝐴 )
6 ordom ⊢ Ord ω
7 ordtri2or ⊢ ( ( Ord 𝐴 ∧ Ord ω ) → ( 𝐴 ∈ ω ∨ ω ⊆ 𝐴 ) )
8 5 6 7 sylancl ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( 𝐴 ∈ ω ∨ ω ⊆ 𝐴 ) )
9 8 ord ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ¬ 𝐴 ∈ ω → ω ⊆ 𝐴 ) )
10 isinfcard ⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) ↔ 𝐴 ∈ ran ℵ )
11 10 biimpi ⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → 𝐴 ∈ ran ℵ )
12 11 expcom ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ω ⊆ 𝐴 → 𝐴 ∈ ran ℵ ) )
13 9 12 syld ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ¬ 𝐴 ∈ ω → 𝐴 ∈ ran ℵ ) )
14 13 orrd ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( 𝐴 ∈ ω ∨ 𝐴 ∈ ran ℵ ) )
15 cardnn ⊢ ( 𝐴 ∈ ω → ( card ‘ 𝐴 ) = 𝐴 )
16 10 bicomi ⊢ ( 𝐴 ∈ ran ℵ ↔ ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) )
17 16 simprbi ⊢ ( 𝐴 ∈ ran ℵ → ( card ‘ 𝐴 ) = 𝐴 )
18 15 17 jaoi ⊢ ( ( 𝐴 ∈ ω ∨ 𝐴 ∈ ran ℵ ) → ( card ‘ 𝐴 ) = 𝐴 )
19 14 18 impbii ⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ ω ∨ 𝐴 ∈ ran ℵ ) )
20 elun ⊢ ( 𝐴 ∈ ( ω ∪ ran ℵ ) ↔ ( 𝐴 ∈ ω ∨ 𝐴 ∈ ran ℵ ) )
21 19 20 bitr4i ⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ ( ω ∪ ran ℵ ) )