Theorem isinfcard

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

	Ref	Expression
Assertion	isinfcard	⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) ↔ 𝐴 ∈ ran ℵ )

Proof

Step	Hyp	Ref	Expression
1		alephfnon	⊢ ℵ Fn On
2		fvelrnb	⊢ ( ℵ Fn On → ( 𝐴 ∈ ran ℵ ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = 𝐴 ) )
3	1 2	ax-mp	⊢ ( 𝐴 ∈ ran ℵ ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = 𝐴 )
4		alephgeom	⊢ ( 𝑥 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝑥 ) )
5	4	biimpi	⊢ ( 𝑥 ∈ On → ω ⊆ ( ℵ ‘ 𝑥 ) )
6		sseq2	⊢ ( 𝐴 = ( ℵ ‘ 𝑥 ) → ( ω ⊆ 𝐴 ↔ ω ⊆ ( ℵ ‘ 𝑥 ) ) )
7	5 6	syl5ibrcom	⊢ ( 𝑥 ∈ On → ( 𝐴 = ( ℵ ‘ 𝑥 ) → ω ⊆ 𝐴 ) )
8	7	rexlimiv	⊢ ( ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) → ω ⊆ 𝐴 )
9	8	pm4.71ri	⊢ ( ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ↔ ( ω ⊆ 𝐴 ∧ ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ) )
10		eqcom	⊢ ( ( ℵ ‘ 𝑥 ) = 𝐴 ↔ 𝐴 = ( ℵ ‘ 𝑥 ) )
11	10	rexbii	⊢ ( ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = 𝐴 ↔ ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) )
12		cardalephex	⊢ ( ω ⊆ 𝐴 → ( ( card ‘ 𝐴 ) = 𝐴 ↔ ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ) )
13	12	pm5.32i	⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) ↔ ( ω ⊆ 𝐴 ∧ ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ) )
14	9 11 13	3bitr4i	⊢ ( ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = 𝐴 ↔ ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) )
15	3 14	bitr2i	⊢ ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) ↔ 𝐴 ∈ ran ℵ )