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