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 ⁡ A = A ↔ A ∈ ω ∪ ran ⁡ ℵ

Proof

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