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 ⊢ℵIsomE,≺Onx∈ran⁡card|ω⊆x

Proof

Step Hyp Ref Expression
1 alephiso ⊢ℵIsomE,EOnx|ω⊆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 ontox|ω⊆x∧card⁡x=x↔ℵ:On⟶1-1 ontox∈ran⁡card|ω⊆x
8 6 7 ax-mp ⊢ℵ:On⟶1-1 ontox|ω⊆x∧card⁡x=x↔ℵ:On⟶1-1 ontox∈ran⁡card|ω⊆x
9 alephon ⊢ℵ⁡z∈On
10 epelg ⊢ℵ⁡z∈On→ℵ⁡yEℵ⁡z↔ℵ⁡y∈ℵ⁡z
11 9 10 mp1i ⊢y∈On∧z∈On→ℵ⁡yEℵ⁡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→ℵ⁡yEℵ⁡z↔ℵ⁡y≺ℵ⁡z
15 14 bibi2d ⊢y∈On∧z∈On→yEz↔ℵ⁡yEℵ⁡z↔yEz↔ℵ⁡y≺ℵ⁡z
16 15 ralbidva ⊢y∈On→∀z∈OnyEz↔ℵ⁡yEℵ⁡z↔∀z∈OnyEz↔ℵ⁡y≺ℵ⁡z
17 16 ralbiia ⊢∀y∈On∀z∈OnyEz↔ℵ⁡yEℵ⁡z↔∀y∈On∀z∈OnyEz↔ℵ⁡y≺ℵ⁡z
18 8 17 anbi12i ⊢ℵ:On⟶1-1 ontox|ω⊆x∧card⁡x=x∧∀y∈On∀z∈OnyEz↔ℵ⁡yEℵ⁡z↔ℵ:On⟶1-1 ontox∈ran⁡card|ω⊆x∧∀y∈On∀z∈OnyEz↔ℵ⁡y≺ℵ⁡z
19 df-isom ⊢ℵIsomE,EOnx|ω⊆x∧card⁡x=x↔ℵ:On⟶1-1 ontox|ω⊆x∧card⁡x=x∧∀y∈On∀z∈OnyEz↔ℵ⁡yEℵ⁡z
20 df-isom ⊢ℵIsomE,≺Onx∈ran⁡card|ω⊆x↔ℵ:On⟶1-1 ontox∈ran⁡card|ω⊆x∧∀y∈On∀z∈OnyEz↔ℵ⁡y≺ℵ⁡z
21 18 19 20 3bitr4i ⊢ℵIsomE,EOnx|ω⊆x∧card⁡x=x↔ℵIsomE,≺Onx∈ran⁡card|ω⊆x
22 1 21 mpbi ⊢ℵIsomE,≺Onx∈ran⁡card|ω⊆x