Metamath Proof Explorer

Theorem smoiso

Description: If F is an isomorphism from an ordinal A onto B , which is a subset of the ordinals, then F is a strictly monotonic function. Exercise 3 in TakeutiZaring p. 50. (Contributed by Andrew Salmon, 24-Nov-2011)

Ref Expression
Assertion smoiso 
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> Smo F )

Proof

Step Hyp Ref Expression
1 isof1o 
 |-  ( F Isom _E , _E ( A , B ) -> F : A -1-1-onto-> B )
2 f1of 
 |-  ( F : A -1-1-onto-> B -> F : A --> B )
3 1 2 syl 
 |-  ( F Isom _E , _E ( A , B ) -> F : A --> B )
4 ffdm 
 |-  ( F : A --> B -> ( F : dom F --> B /\ dom F C_ A ) )
5 4 simpld 
 |-  ( F : A --> B -> F : dom F --> B )
6 fss 
 |-  ( ( F : dom F --> B /\ B C_ On ) -> F : dom F --> On )
7 5 6 sylan 
 |-  ( ( F : A --> B /\ B C_ On ) -> F : dom F --> On )
8 7 3adant2 
 |-  ( ( F : A --> B /\ Ord A /\ B C_ On ) -> F : dom F --> On )
9 3 8 syl3an1 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> F : dom F --> On )
10 fdm 
 |-  ( F : A --> B -> dom F = A )
11 10 eqcomd 
 |-  ( F : A --> B -> A = dom F )
12 ordeq 
 |-  ( A = dom F -> ( Ord A <-> Ord dom F ) )
13 1 2 11 12 4syl 
 |-  ( F Isom _E , _E ( A , B ) -> ( Ord A <-> Ord dom F ) )
14 13 biimpa 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A ) -> Ord dom F )
15 14 3adant3 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> Ord dom F )
16 10 eleq2d 
 |-  ( F : A --> B -> ( x e. dom F <-> x e. A ) )
17 10 eleq2d 
 |-  ( F : A --> B -> ( y e. dom F <-> y e. A ) )
18 16 17 anbi12d 
 |-  ( F : A --> B -> ( ( x e. dom F /\ y e. dom F ) <-> ( x e. A /\ y e. A ) ) )
19 1 2 18 3syl 
 |-  ( F Isom _E , _E ( A , B ) -> ( ( x e. dom F /\ y e. dom F ) <-> ( x e. A /\ y e. A ) ) )
20 isorel 
 |-  ( ( F Isom _E , _E ( A , B ) /\ ( x e. A /\ y e. A ) ) -> ( x _E y <-> ( F ` x ) _E ( F ` y ) ) )
21 epel 
 |-  ( x _E y <-> x e. y )
22 fvex 
 |-  ( F ` y ) e. _V
23 22 epeli 
 |-  ( ( F ` x ) _E ( F ` y ) <-> ( F ` x ) e. ( F ` y ) )
24 20 21 23 3bitr3g 
 |-  ( ( F Isom _E , _E ( A , B ) /\ ( x e. A /\ y e. A ) ) -> ( x e. y <-> ( F ` x ) e. ( F ` y ) ) )
25 24 biimpd 
 |-  ( ( F Isom _E , _E ( A , B ) /\ ( x e. A /\ y e. A ) ) -> ( x e. y -> ( F ` x ) e. ( F ` y ) ) )
26 25 ex 
 |-  ( F Isom _E , _E ( A , B ) -> ( ( x e. A /\ y e. A ) -> ( x e. y -> ( F ` x ) e. ( F ` y ) ) ) )
27 19 26 sylbid 
 |-  ( F Isom _E , _E ( A , B ) -> ( ( x e. dom F /\ y e. dom F ) -> ( x e. y -> ( F ` x ) e. ( F ` y ) ) ) )
28 27 ralrimivv 
 |-  ( F Isom _E , _E ( A , B ) -> A. x e. dom F A. y e. dom F ( x e. y -> ( F ` x ) e. ( F ` y ) ) )
29 28 3ad2ant1 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> A. x e. dom F A. y e. dom F ( x e. y -> ( F ` x ) e. ( F ` y ) ) )
30 df-smo 
 |-  ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. dom F ( x e. y -> ( F ` x ) e. ( F ` y ) ) ) )
31 9 15 29 30 syl3anbrc 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> Smo F )