# Metamath Proof Explorer

## Theorem smoiso2

Description: The strictly monotone ordinal functions are also isomorphisms of subclasses of On equipped with the membership relation. (Contributed by Mario Carneiro, 20-Mar-2013)

Ref Expression
Assertion smoiso2 ${⊢}\left(\mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\to \left(\left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)↔{F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fof ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to {F}:{A}⟶{B}$
2 smo11 ${⊢}\left({F}:{A}⟶{B}\wedge \mathrm{Smo}{F}\right)\to {F}:{A}\underset{1-1}{⟶}{B}$
3 1 2 sylan ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\to {F}:{A}\underset{1-1}{⟶}{B}$
4 simpl ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\to {F}:{A}\underset{onto}{⟶}{B}$
5 df-f1o ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {F}:{A}\underset{onto}{⟶}{B}\right)$
6 3 4 5 sylanbrc ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\to {F}:{A}\underset{1-1 onto}{⟶}{B}$
7 6 adantl ${⊢}\left(\left(\mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\wedge \left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\right)\to {F}:{A}\underset{1-1 onto}{⟶}{B}$
8 fofn ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to {F}Fn{A}$
9 smoord ${⊢}\left(\left({F}Fn{A}\wedge \mathrm{Smo}{F}\right)\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({x}\in {y}↔{F}\left({x}\right)\in {F}\left({y}\right)\right)$
10 epel ${⊢}{x}\mathrm{E}{y}↔{x}\in {y}$
11 fvex ${⊢}{F}\left({y}\right)\in \mathrm{V}$
12 11 epeli ${⊢}{F}\left({x}\right)\mathrm{E}{F}\left({y}\right)↔{F}\left({x}\right)\in {F}\left({y}\right)$
13 9 10 12 3bitr4g ${⊢}\left(\left({F}Fn{A}\wedge \mathrm{Smo}{F}\right)\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({x}\mathrm{E}{y}↔{F}\left({x}\right)\mathrm{E}{F}\left({y}\right)\right)$
14 13 ralrimivva ${⊢}\left({F}Fn{A}\wedge \mathrm{Smo}{F}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{E}{y}↔{F}\left({x}\right)\mathrm{E}{F}\left({y}\right)\right)$
15 8 14 sylan ${⊢}\left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{E}{y}↔{F}\left({x}\right)\mathrm{E}{F}\left({y}\right)\right)$
16 15 adantl ${⊢}\left(\left(\mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\wedge \left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{E}{y}↔{F}\left({x}\right)\mathrm{E}{F}\left({y}\right)\right)$
17 df-isom ${⊢}{F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)↔\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{E}{y}↔{F}\left({x}\right)\mathrm{E}{F}\left({y}\right)\right)\right)$
18 7 16 17 sylanbrc ${⊢}\left(\left(\mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\wedge \left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\right)\to {F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)$
19 18 ex ${⊢}\left(\mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\to \left(\left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\to {F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\right)$
20 isof1o ${⊢}{F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\to {F}:{A}\underset{1-1 onto}{⟶}{B}$
21 f1ofo ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {F}:{A}\underset{onto}{⟶}{B}$
22 20 21 syl ${⊢}{F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\to {F}:{A}\underset{onto}{⟶}{B}$
23 22 3ad2ant1 ${⊢}\left({F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\wedge \mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\to {F}:{A}\underset{onto}{⟶}{B}$
24 smoiso ${⊢}\left({F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\wedge \mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\to \mathrm{Smo}{F}$
25 23 24 jca ${⊢}\left({F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\wedge \mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\to \left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)$
26 25 3expib ${⊢}{F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\to \left(\left(\mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\to \left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\right)$
27 26 com12 ${⊢}\left(\mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\to \left({F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\to \left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)\right)$
28 19 27 impbid ${⊢}\left(\mathrm{Ord}{A}\wedge {B}\subseteq \mathrm{On}\right)\to \left(\left({F}:{A}\underset{onto}{⟶}{B}\wedge \mathrm{Smo}{F}\right)↔{F}{Isom}_{\mathrm{E},\mathrm{E}}\left({A},{B}\right)\right)$