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 x | ω ⊆ x ∧ card ⁡ x = x

Proof

Step Hyp Ref Expression
1 alephfnon ⊢ ℵ Fn On
2 isinfcard ⊢ ω ⊆ x ∧ card ⁡ x = x ↔ x ∈ ran ⁡ ℵ
3 2 bicomi ⊢ x ∈ ran ⁡ ℵ ↔ ω ⊆ x ∧ card ⁡ x = x
4 3 eqabi ⊢ ran ⁡ ℵ = x | ω ⊆ x ∧ card ⁡ x = x
5 df-fo ⊢ ℵ : On ⟶ onto x | ω ⊆ x ∧ card ⁡ x = x ↔ ℵ Fn On ∧ ran ⁡ ℵ = x | ω ⊆ x ∧ card ⁡ x = x
6 1 4 5 mpbir2an ⊢ ℵ : On ⟶ onto x | ω ⊆ x ∧ card ⁡ x = x
7 fof ⊢ ℵ : On ⟶ onto x | ω ⊆ x ∧ card ⁡ x = x → ℵ : On ⟶ x | ω ⊆ x ∧ card ⁡ x = x
8 6 7 ax-mp ⊢ ℵ : On ⟶ x | ω ⊆ x ∧ card ⁡ x = x
9 aleph11 ⊢ y ∈ On ∧ z ∈ On → ℵ ⁡ y = ℵ ⁡ z ↔ y = z
10 9 biimpd ⊢ y ∈ On ∧ z ∈ On → ℵ ⁡ y = ℵ ⁡ z → y = z
11 10 rgen2 ⊢ ∀ y ∈ On ∀ z ∈ On ℵ ⁡ y = ℵ ⁡ z → y = z
12 dff13 ⊢ ℵ : On ⟶ 1-1 x | ω ⊆ x ∧ card ⁡ x = x ↔ ℵ : On ⟶ x | ω ⊆ x ∧ card ⁡ x = x ∧ ∀ y ∈ On ∀ z ∈ On ℵ ⁡ y = ℵ ⁡ z → y = z
13 8 11 12 mpbir2an ⊢ ℵ : On ⟶ 1-1 x | ω ⊆ x ∧ card ⁡ x = x
14 df-f1o ⊢ ℵ : On ⟶ 1-1 onto x | ω ⊆ x ∧ card ⁡ x = x ↔ ℵ : On ⟶ 1-1 x | ω ⊆ x ∧ card ⁡ x = x ∧ ℵ : On ⟶ onto x | ω ⊆ x ∧ card ⁡ x = x
15 13 6 14 mpbir2an ⊢ ℵ : On ⟶ 1-1 onto x | ω ⊆ x ∧ card ⁡ x = x
16 alephord2 ⊢ y ∈ On ∧ z ∈ On → y ∈ z ↔ ℵ ⁡ y ∈ ℵ ⁡ z
17 epel ⊢ y E z ↔ y ∈ z
18 fvex ⊢ ℵ ⁡ z ∈ V
19 18 epeli ⊢ ℵ ⁡ y E ℵ ⁡ z ↔ ℵ ⁡ y ∈ ℵ ⁡ z
20 16 17 19 3bitr4g ⊢ y ∈ On ∧ z ∈ On → y E z ↔ ℵ ⁡ y E ℵ ⁡ z
21 20 rgen2 ⊢ ∀ y ∈ On ∀ z ∈ On y E z ↔ ℵ ⁡ y E ℵ ⁡ z
22 df-isom ⊢ ℵ Isom E , E On x | ω ⊆ x ∧ card ⁡ x = x ↔ ℵ : On ⟶ 1-1 onto x | ω ⊆ x ∧ card ⁡ x = x ∧ ∀ y ∈ On ∀ z ∈ On y E z ↔ ℵ ⁡ y E ℵ ⁡ z
23 15 21 22 mpbir2an ⊢ ℵ Isom E , E On x | ω ⊆ x ∧ card ⁡ x = x