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

Metamath Proof Explorer

Theorem infenaleph

Description: An infinite numerable set is equinumerous to an infinite initial ordinal. (Contributed by Jeff Hankins, 23-Oct-2009) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infenaleph ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∃ 𝑥 ∈ ran ℵ 𝑥 ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 cardidm ⊢ ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 )
2 cardom ⊢ ( card ‘ ω ) = ω
3 simpr ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ω ≼ 𝐴 )
4 omelon ⊢ ω ∈ On
5 onenon ⊢ ( ω ∈ On → ω ∈ dom card )
6 4 5 ax-mp ⊢ ω ∈ dom card
7 simpl ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝐴 ∈ dom card )
8 carddom2 ⊢ ( ( ω ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( card ‘ ω ) ⊆ ( card ‘ 𝐴 ) ↔ ω ≼ 𝐴 ) )
9 6 7 8 sylancr ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( card ‘ ω ) ⊆ ( card ‘ 𝐴 ) ↔ ω ≼ 𝐴 ) )
10 3 9 mpbird ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( card ‘ ω ) ⊆ ( card ‘ 𝐴 ) )
11 2 10 eqsstrrid ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ω ⊆ ( card ‘ 𝐴 ) )
12 cardalephex ⊢ ( ω ⊆ ( card ‘ 𝐴 ) → ( ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) ↔ ∃ 𝑥 ∈ On ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) ) )
13 11 12 syl ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) ↔ ∃ 𝑥 ∈ On ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) ) )
14 1 13 mpbii ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∃ 𝑥 ∈ On ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) )
15 eqcom ⊢ ( ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) )
16 15 rexbii ⊢ ( ∃ 𝑥 ∈ On ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) )
17 14 16 sylib ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) )
18 alephfnon ⊢ ℵ Fn On
19 fvelrnb ⊢ ( ℵ Fn On → ( ( card ‘ 𝐴 ) ∈ ran ℵ ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) ) )
20 18 19 ax-mp ⊢ ( ( card ‘ 𝐴 ) ∈ ran ℵ ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) )
21 17 20 sylibr ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( card ‘ 𝐴 ) ∈ ran ℵ )
22 cardid2 ⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
23 22 adantr ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( card ‘ 𝐴 ) ≈ 𝐴 )
24 breq1 ⊢ ( 𝑥 = ( card ‘ 𝐴 ) → ( 𝑥 ≈ 𝐴 ↔ ( card ‘ 𝐴 ) ≈ 𝐴 ) )
25 24 rspcev ⊢ ( ( ( card ‘ 𝐴 ) ∈ ran ℵ ∧ ( card ‘ 𝐴 ) ≈ 𝐴 ) → ∃ 𝑥 ∈ ran ℵ 𝑥 ≈ 𝐴 )
26 21 23 25 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∃ 𝑥 ∈ ran ℵ 𝑥 ≈ 𝐴 )