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

Metamath Proof Explorer

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