Metamath Proof Explorer


Theorem smores2

Description: A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013)

Ref Expression
Assertion smores2
|- ( ( Smo F /\ Ord A ) -> Smo ( F |` A ) )

Proof

Step Hyp Ref Expression
1 dfsmo2
 |-  ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) )
2 1 simp1bi
 |-  ( Smo F -> F : dom F --> On )
3 2 ffund
 |-  ( Smo F -> Fun F )
4 funres
 |-  ( Fun F -> Fun ( F |` A ) )
5 4 funfnd
 |-  ( Fun F -> ( F |` A ) Fn dom ( F |` A ) )
6 3 5 syl
 |-  ( Smo F -> ( F |` A ) Fn dom ( F |` A ) )
7 df-ima
 |-  ( F " A ) = ran ( F |` A )
8 imassrn
 |-  ( F " A ) C_ ran F
9 7 8 eqsstrri
 |-  ran ( F |` A ) C_ ran F
10 2 frnd
 |-  ( Smo F -> ran F C_ On )
11 9 10 sstrid
 |-  ( Smo F -> ran ( F |` A ) C_ On )
12 df-f
 |-  ( ( F |` A ) : dom ( F |` A ) --> On <-> ( ( F |` A ) Fn dom ( F |` A ) /\ ran ( F |` A ) C_ On ) )
13 6 11 12 sylanbrc
 |-  ( Smo F -> ( F |` A ) : dom ( F |` A ) --> On )
14 13 adantr
 |-  ( ( Smo F /\ Ord A ) -> ( F |` A ) : dom ( F |` A ) --> On )
15 smodm
 |-  ( Smo F -> Ord dom F )
16 ordin
 |-  ( ( Ord A /\ Ord dom F ) -> Ord ( A i^i dom F ) )
17 dmres
 |-  dom ( F |` A ) = ( A i^i dom F )
18 ordeq
 |-  ( dom ( F |` A ) = ( A i^i dom F ) -> ( Ord dom ( F |` A ) <-> Ord ( A i^i dom F ) ) )
19 17 18 ax-mp
 |-  ( Ord dom ( F |` A ) <-> Ord ( A i^i dom F ) )
20 16 19 sylibr
 |-  ( ( Ord A /\ Ord dom F ) -> Ord dom ( F |` A ) )
21 20 ancoms
 |-  ( ( Ord dom F /\ Ord A ) -> Ord dom ( F |` A ) )
22 15 21 sylan
 |-  ( ( Smo F /\ Ord A ) -> Ord dom ( F |` A ) )
23 resss
 |-  ( F |` A ) C_ F
24 dmss
 |-  ( ( F |` A ) C_ F -> dom ( F |` A ) C_ dom F )
25 23 24 ax-mp
 |-  dom ( F |` A ) C_ dom F
26 1 simp3bi
 |-  ( Smo F -> A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) )
27 ssralv
 |-  ( dom ( F |` A ) C_ dom F -> ( A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) -> A. x e. dom ( F |` A ) A. y e. x ( F ` y ) e. ( F ` x ) ) )
28 25 26 27 mpsyl
 |-  ( Smo F -> A. x e. dom ( F |` A ) A. y e. x ( F ` y ) e. ( F ` x ) )
29 28 adantr
 |-  ( ( Smo F /\ Ord A ) -> A. x e. dom ( F |` A ) A. y e. x ( F ` y ) e. ( F ` x ) )
30 ordtr1
 |-  ( Ord dom ( F |` A ) -> ( ( y e. x /\ x e. dom ( F |` A ) ) -> y e. dom ( F |` A ) ) )
31 22 30 syl
 |-  ( ( Smo F /\ Ord A ) -> ( ( y e. x /\ x e. dom ( F |` A ) ) -> y e. dom ( F |` A ) ) )
32 inss1
 |-  ( A i^i dom F ) C_ A
33 17 32 eqsstri
 |-  dom ( F |` A ) C_ A
34 33 sseli
 |-  ( y e. dom ( F |` A ) -> y e. A )
35 31 34 syl6
 |-  ( ( Smo F /\ Ord A ) -> ( ( y e. x /\ x e. dom ( F |` A ) ) -> y e. A ) )
36 35 expcomd
 |-  ( ( Smo F /\ Ord A ) -> ( x e. dom ( F |` A ) -> ( y e. x -> y e. A ) ) )
37 36 imp31
 |-  ( ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) /\ y e. x ) -> y e. A )
38 37 fvresd
 |-  ( ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) /\ y e. x ) -> ( ( F |` A ) ` y ) = ( F ` y ) )
39 33 sseli
 |-  ( x e. dom ( F |` A ) -> x e. A )
40 39 fvresd
 |-  ( x e. dom ( F |` A ) -> ( ( F |` A ) ` x ) = ( F ` x ) )
41 40 ad2antlr
 |-  ( ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) /\ y e. x ) -> ( ( F |` A ) ` x ) = ( F ` x ) )
42 38 41 eleq12d
 |-  ( ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) /\ y e. x ) -> ( ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) <-> ( F ` y ) e. ( F ` x ) ) )
43 42 ralbidva
 |-  ( ( ( Smo F /\ Ord A ) /\ x e. dom ( F |` A ) ) -> ( A. y e. x ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) <-> A. y e. x ( F ` y ) e. ( F ` x ) ) )
44 43 ralbidva
 |-  ( ( Smo F /\ Ord A ) -> ( A. x e. dom ( F |` A ) A. y e. x ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) <-> A. x e. dom ( F |` A ) A. y e. x ( F ` y ) e. ( F ` x ) ) )
45 29 44 mpbird
 |-  ( ( Smo F /\ Ord A ) -> A. x e. dom ( F |` A ) A. y e. x ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) )
46 dfsmo2
 |-  ( Smo ( F |` A ) <-> ( ( F |` A ) : dom ( F |` A ) --> On /\ Ord dom ( F |` A ) /\ A. x e. dom ( F |` A ) A. y e. x ( ( F |` A ) ` y ) e. ( ( F |` A ) ` x ) ) )
47 14 22 45 46 syl3anbrc
 |-  ( ( Smo F /\ Ord A ) -> Smo ( F |` A ) )