Metamath Proof Explorer


Theorem alephiso

Description: Aleph is an order isomorphism of the class of ordinal numbers onto the class of infinite cardinals. Definition 10.27 of TakeutiZaring p. 90. (Contributed by NM, 3-Aug-2004)

Ref Expression
Assertion alephiso ℵ Isom E , E ( On , { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 alephfnon ℵ Fn On
2 isinfcard ( ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) ↔ 𝑥 ∈ ran ℵ )
3 2 bicomi ( 𝑥 ∈ ran ℵ ↔ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) )
4 3 abbi2i ran ℵ = { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) }
5 df-fo ( ℵ : On –onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ↔ ( ℵ Fn On ∧ ran ℵ = { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) )
6 1 4 5 mpbir2an ℵ : On –onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) }
7 fof ( ℵ : On –onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } → ℵ : On ⟶ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } )
8 6 7 ax-mp ℵ : On ⟶ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) }
9 aleph11 ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( ℵ ‘ 𝑦 ) = ( ℵ ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) )
10 9 biimpd ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( ℵ ‘ 𝑦 ) = ( ℵ ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
11 10 rgen2 𝑦 ∈ On ∀ 𝑧 ∈ On ( ( ℵ ‘ 𝑦 ) = ( ℵ ‘ 𝑧 ) → 𝑦 = 𝑧 )
12 dff13 ( ℵ : On –1-1→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ↔ ( ℵ : On ⟶ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ∧ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( ( ℵ ‘ 𝑦 ) = ( ℵ ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
13 8 11 12 mpbir2an ℵ : On –1-1→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) }
14 df-f1o ( ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ↔ ( ℵ : On –1-1→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ∧ ℵ : On –onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) )
15 13 6 14 mpbir2an ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) }
16 alephord2 ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦𝑧 ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑧 ) ) )
17 epel ( 𝑦 E 𝑧𝑦𝑧 )
18 fvex ( ℵ ‘ 𝑧 ) ∈ V
19 18 epeli ( ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑧 ) )
20 16 17 19 3bitr4g ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) )
21 20 rgen2 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) )
22 df-isom ( ℵ Isom E , E ( On , { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) ↔ ( ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ∧ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) ) )
23 15 21 22 mpbir2an ℵ Isom E , E ( On , { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } )