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 ) )