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 )