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 
|- ( ( Ord A /\ B C_ On ) -> ( ( F : A -onto-> B /\ Smo F ) <-> F Isom _E , _E ( A , B ) ) )

Proof

Step Hyp Ref Expression
1 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
2 smo11 
 |-  ( ( F : A --> B /\ Smo F ) -> F : A -1-1-> B )
3 1 2 sylan 
 |-  ( ( F : A -onto-> B /\ Smo F ) -> F : A -1-1-> B )
4 simpl 
 |-  ( ( F : A -onto-> B /\ Smo F ) -> F : A -onto-> B )
5 df-f1o 
 |-  ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
6 3 4 5 sylanbrc 
 |-  ( ( F : A -onto-> B /\ Smo F ) -> F : A -1-1-onto-> B )
7 6 adantl 
 |-  ( ( ( Ord A /\ B C_ On ) /\ ( F : A -onto-> B /\ Smo F ) ) -> F : A -1-1-onto-> B )
8 fofn 
 |-  ( F : A -onto-> B -> F Fn A )
9 smoord 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( x e. A /\ y e. A ) ) -> ( x e. y <-> ( F ` x ) e. ( F ` y ) ) )
10 epel 
 |-  ( x _E y <-> x e. y )
11 fvex 
 |-  ( F ` y ) e. _V
12 11 epeli 
 |-  ( ( F ` x ) _E ( F ` y ) <-> ( F ` x ) e. ( F ` y ) )
13 9 10 12 3bitr4g 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( x e. A /\ y e. A ) ) -> ( x _E y <-> ( F ` x ) _E ( F ` y ) ) )
14 13 ralrimivva 
 |-  ( ( F Fn A /\ Smo F ) -> A. x e. A A. y e. A ( x _E y <-> ( F ` x ) _E ( F ` y ) ) )
15 8 14 sylan 
 |-  ( ( F : A -onto-> B /\ Smo F ) -> A. x e. A A. y e. A ( x _E y <-> ( F ` x ) _E ( F ` y ) ) )
16 15 adantl 
 |-  ( ( ( Ord A /\ B C_ On ) /\ ( F : A -onto-> B /\ Smo F ) ) -> A. x e. A A. y e. A ( x _E y <-> ( F ` x ) _E ( F ` y ) ) )
17 df-isom 
 |-  ( F Isom _E , _E ( A , B ) <-> ( F : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x _E y <-> ( F ` x ) _E ( F ` y ) ) ) )
18 7 16 17 sylanbrc 
 |-  ( ( ( Ord A /\ B C_ On ) /\ ( F : A -onto-> B /\ Smo F ) ) -> F Isom _E , _E ( A , B ) )
19 18 ex 
 |-  ( ( Ord A /\ B C_ On ) -> ( ( F : A -onto-> B /\ Smo F ) -> F Isom _E , _E ( A , B ) ) )
20 isof1o 
 |-  ( F Isom _E , _E ( A , B ) -> F : A -1-1-onto-> B )
21 f1ofo 
 |-  ( F : A -1-1-onto-> B -> F : A -onto-> B )
22 20 21 syl 
 |-  ( F Isom _E , _E ( A , B ) -> F : A -onto-> B )
23 22 3ad2ant1 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> F : A -onto-> B )
24 smoiso 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> Smo F )
25 23 24 jca 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> ( F : A -onto-> B /\ Smo F ) )
26 25 3expib 
 |-  ( F Isom _E , _E ( A , B ) -> ( ( Ord A /\ B C_ On ) -> ( F : A -onto-> B /\ Smo F ) ) )
27 26 com12 
 |-  ( ( Ord A /\ B C_ On ) -> ( F Isom _E , _E ( A , B ) -> ( F : A -onto-> B /\ Smo F ) ) )
28 19 27 impbid 
 |-  ( ( Ord A /\ B C_ On ) -> ( ( F : A -onto-> B /\ Smo F ) <-> F Isom _E , _E ( A , B ) ) )