# 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 ${⊢}\aleph {Isom}_{\mathrm{E},\prec }\left(\mathrm{On},\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 alephiso ${⊢}\aleph {Isom}_{\mathrm{E},\mathrm{E}}\left(\mathrm{On},\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}\right)$
2 iscard4 ${⊢}\mathrm{card}\left({x}\right)={x}↔{x}\in \mathrm{ran}\mathrm{card}$
3 2 anbi1ci ${⊢}\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)↔\left({x}\in \mathrm{ran}\mathrm{card}\wedge \mathrm{\omega }\subseteq {x}\right)$
4 3 abbii ${⊢}\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}=\left\{{x}|\left({x}\in \mathrm{ran}\mathrm{card}\wedge \mathrm{\omega }\subseteq {x}\right)\right\}$
5 df-rab ${⊢}\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}=\left\{{x}|\left({x}\in \mathrm{ran}\mathrm{card}\wedge \mathrm{\omega }\subseteq {x}\right)\right\}$
6 4 5 eqtr4i ${⊢}\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}=\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}$
7 f1oeq3 ${⊢}\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}=\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}\to \left(\aleph :\mathrm{On}\underset{1-1 onto}{⟶}\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}↔\aleph :\mathrm{On}\underset{1-1 onto}{⟶}\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}\right)$
8 6 7 ax-mp ${⊢}\aleph :\mathrm{On}\underset{1-1 onto}{⟶}\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}↔\aleph :\mathrm{On}\underset{1-1 onto}{⟶}\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}$
9 alephon ${⊢}\aleph \left({z}\right)\in \mathrm{On}$
10 epelg ${⊢}\aleph \left({z}\right)\in \mathrm{On}\to \left(\aleph \left({y}\right)\mathrm{E}\aleph \left({z}\right)↔\aleph \left({y}\right)\in \aleph \left({z}\right)\right)$
11 9 10 mp1i ${⊢}\left({y}\in \mathrm{On}\wedge {z}\in \mathrm{On}\right)\to \left(\aleph \left({y}\right)\mathrm{E}\aleph \left({z}\right)↔\aleph \left({y}\right)\in \aleph \left({z}\right)\right)$
12 alephord2 ${⊢}\left({y}\in \mathrm{On}\wedge {z}\in \mathrm{On}\right)\to \left({y}\in {z}↔\aleph \left({y}\right)\in \aleph \left({z}\right)\right)$
13 alephord ${⊢}\left({y}\in \mathrm{On}\wedge {z}\in \mathrm{On}\right)\to \left({y}\in {z}↔\aleph \left({y}\right)\prec \aleph \left({z}\right)\right)$
14 11 12 13 3bitr2d ${⊢}\left({y}\in \mathrm{On}\wedge {z}\in \mathrm{On}\right)\to \left(\aleph \left({y}\right)\mathrm{E}\aleph \left({z}\right)↔\aleph \left({y}\right)\prec \aleph \left({z}\right)\right)$
15 14 bibi2d ${⊢}\left({y}\in \mathrm{On}\wedge {z}\in \mathrm{On}\right)\to \left(\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\mathrm{E}\aleph \left({z}\right)\right)↔\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\prec \aleph \left({z}\right)\right)\right)$
16 15 ralbidva ${⊢}{y}\in \mathrm{On}\to \left(\forall {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\mathrm{E}\aleph \left({z}\right)\right)↔\forall {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\prec \aleph \left({z}\right)\right)\right)$
17 16 ralbiia ${⊢}\forall {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\mathrm{E}\aleph \left({z}\right)\right)↔\forall {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\prec \aleph \left({z}\right)\right)$
18 8 17 anbi12i ${⊢}\left(\aleph :\mathrm{On}\underset{1-1 onto}{⟶}\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}\wedge \forall {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\mathrm{E}\aleph \left({z}\right)\right)\right)↔\left(\aleph :\mathrm{On}\underset{1-1 onto}{⟶}\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}\wedge \forall {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\prec \aleph \left({z}\right)\right)\right)$
19 df-isom ${⊢}\aleph {Isom}_{\mathrm{E},\mathrm{E}}\left(\mathrm{On},\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}\right)↔\left(\aleph :\mathrm{On}\underset{1-1 onto}{⟶}\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}\wedge \forall {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\mathrm{E}\aleph \left({z}\right)\right)\right)$
20 df-isom ${⊢}\aleph {Isom}_{\mathrm{E},\prec }\left(\mathrm{On},\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}\right)↔\left(\aleph :\mathrm{On}\underset{1-1 onto}{⟶}\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}\wedge \forall {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{E}{z}↔\aleph \left({y}\right)\prec \aleph \left({z}\right)\right)\right)$
21 18 19 20 3bitr4i ${⊢}\aleph {Isom}_{\mathrm{E},\mathrm{E}}\left(\mathrm{On},\left\{{x}|\left(\mathrm{\omega }\subseteq {x}\wedge \mathrm{card}\left({x}\right)={x}\right)\right\}\right)↔\aleph {Isom}_{\mathrm{E},\prec }\left(\mathrm{On},\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}\right)$
22 1 21 mpbi ${⊢}\aleph {Isom}_{\mathrm{E},\prec }\left(\mathrm{On},\left\{{x}\in \mathrm{ran}\mathrm{card}|\mathrm{\omega }\subseteq {x}\right\}\right)$