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

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 eqabi ⊢ 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 ‘ 𝑥 ) = 𝑥 ) } )