Metamath Proof Explorer

Theorem alephiso2

Description: aleph is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023)

Ref Expression
Assertion alephiso2 ⊢ ℵ Isom E , ≺ On x ∈ ran ⁡ card | ω ⊆ x

Proof

Step Hyp Ref Expression
1 alephiso ⊢ ℵ Isom E , E On x | ω ⊆ x ∧ card ⁡ x = x
2 iscard4 ⊢ card ⁡ x = x ↔ x ∈ ran ⁡ card
3 2 anbi1ci ⊢ ω ⊆ x ∧ card ⁡ x = x ↔ x ∈ ran ⁡ card ∧ ω ⊆ x
4 3 abbii ⊢ x | ω ⊆ x ∧ card ⁡ x = x = x | x ∈ ran ⁡ card ∧ ω ⊆ x
5 df-rab ⊢ x ∈ ran ⁡ card | ω ⊆ x = x | x ∈ ran ⁡ card ∧ ω ⊆ x
6 4 5 eqtr4i ⊢ x | ω ⊆ x ∧ card ⁡ x = x = x ∈ ran ⁡ card | ω ⊆ x
7 f1oeq3 ⊢ x | ω ⊆ x ∧ card ⁡ x = x = x ∈ ran ⁡ card | ω ⊆ x → ℵ : On ⟶ 1-1 onto x | ω ⊆ x ∧ card ⁡ x = x ↔ ℵ : On ⟶ 1-1 onto x ∈ ran ⁡ card | ω ⊆ x
8 6 7 ax-mp ⊢ ℵ : On ⟶ 1-1 onto x | ω ⊆ x ∧ card ⁡ x = x ↔ ℵ : On ⟶ 1-1 onto x ∈ ran ⁡ card | ω ⊆ x
9 alephon ⊢ ℵ ⁡ z ∈ On
10 epelg ⊢ ℵ ⁡ z ∈ On → ℵ ⁡ y E ℵ ⁡ z ↔ ℵ ⁡ y ∈ ℵ ⁡ z
11 9 10 mp1i ⊢ y ∈ On ∧ z ∈ On → ℵ ⁡ y E ℵ ⁡ z ↔ ℵ ⁡ y ∈ ℵ ⁡ z
12 alephord2 ⊢ y ∈ On ∧ z ∈ On → y ∈ z ↔ ℵ ⁡ y ∈ ℵ ⁡ z
13 alephord ⊢ y ∈ On ∧ z ∈ On → y ∈ z ↔ ℵ ⁡ y ≺ ℵ ⁡ z
14 11 12 13 3bitr2d ⊢ y ∈ On ∧ z ∈ On → ℵ ⁡ y E ℵ ⁡ z ↔ ℵ ⁡ y ≺ ℵ ⁡ z
15 14 bibi2d ⊢ y ∈ On ∧ z ∈ On → y E z ↔ ℵ ⁡ y E ℵ ⁡ z ↔ y E z ↔ ℵ ⁡ y ≺ ℵ ⁡ z
16 15 ralbidva ⊢ y ∈ On → ∀ z ∈ On y E z ↔ ℵ ⁡ y E ℵ ⁡ z ↔ ∀ z ∈ On y E z ↔ ℵ ⁡ y ≺ ℵ ⁡ z
17 16 ralbiia ⊢ ∀ y ∈ On ∀ z ∈ On y E z ↔ ℵ ⁡ y E ℵ ⁡ z ↔ ∀ y ∈ On ∀ z ∈ On y E z ↔ ℵ ⁡ y ≺ ℵ ⁡ z
18 8 17 anbi12i ⊢ ℵ : On ⟶ 1-1 onto x | ω ⊆ x ∧ card ⁡ x = x ∧ ∀ y ∈ On ∀ z ∈ On y E z ↔ ℵ ⁡ y E ℵ ⁡ z ↔ ℵ : On ⟶ 1-1 onto x ∈ ran ⁡ card | ω ⊆ x ∧ ∀ y ∈ On ∀ z ∈ On y E z ↔ ℵ ⁡ y ≺ ℵ ⁡ z
19 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
20 df-isom ⊢ ℵ Isom E , ≺ On x ∈ ran ⁡ card | ω ⊆ x ↔ ℵ : On ⟶ 1-1 onto x ∈ ran ⁡ card | ω ⊆ x ∧ ∀ y ∈ On ∀ z ∈ On y E z ↔ ℵ ⁡ y ≺ ℵ ⁡ z
21 18 19 20 3bitr4i ⊢ ℵ Isom E , E On x | ω ⊆ x ∧ card ⁡ x = x ↔ ℵ Isom E , ≺ On x ∈ ran ⁡ card | ω ⊆ x
22 1 21 mpbi ⊢ ℵ Isom E , ≺ On x ∈ ran ⁡ card | ω ⊆ x