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 ⊢ A ∈ dom ⁡ card ∧ ω ≼ A → ∃ x ∈ ran ⁡ ℵ x ≈ A

Proof

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