Metamath Proof Explorer

Theorem smores

Description: A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011) (Proof shortened by Mario Carneiro, 5-Dec-2016)

Ref Expression
Assertion smores 
|- ( ( Smo A /\ B e. dom A ) -> Smo ( A |` B ) )

Proof

Step Hyp Ref Expression
1 funres 
 |-  ( Fun A -> Fun ( A |` B ) )
2 funfn 
 |-  ( Fun A <-> A Fn dom A )
3 funfn 
 |-  ( Fun ( A |` B ) <-> ( A |` B ) Fn dom ( A |` B ) )
4 1 2 3 3imtr3i 
 |-  ( A Fn dom A -> ( A |` B ) Fn dom ( A |` B ) )
5 rnresss 
 |-  ran ( A |` B ) C_ ran A
6 sstr 
 |-  ( ( ran ( A |` B ) C_ ran A /\ ran A C_ On ) -> ran ( A |` B ) C_ On )
7 5 6 mpan 
 |-  ( ran A C_ On -> ran ( A |` B ) C_ On )
8 4 7 anim12i 
 |-  ( ( A Fn dom A /\ ran A C_ On ) -> ( ( A |` B ) Fn dom ( A |` B ) /\ ran ( A |` B ) C_ On ) )
9 df-f 
 |-  ( A : dom A --> On <-> ( A Fn dom A /\ ran A C_ On ) )
10 df-f 
 |-  ( ( A |` B ) : dom ( A |` B ) --> On <-> ( ( A |` B ) Fn dom ( A |` B ) /\ ran ( A |` B ) C_ On ) )
11 8 9 10 3imtr4i 
 |-  ( A : dom A --> On -> ( A |` B ) : dom ( A |` B ) --> On )
12 11 a1i 
 |-  ( B e. dom A -> ( A : dom A --> On -> ( A |` B ) : dom ( A |` B ) --> On ) )
13 ordelord 
 |-  ( ( Ord dom A /\ B e. dom A ) -> Ord B )
14 13 expcom 
 |-  ( B e. dom A -> ( Ord dom A -> Ord B ) )
15 ordin 
 |-  ( ( Ord B /\ Ord dom A ) -> Ord ( B i^i dom A ) )
16 15 ex 
 |-  ( Ord B -> ( Ord dom A -> Ord ( B i^i dom A ) ) )
17 14 16 syli 
 |-  ( B e. dom A -> ( Ord dom A -> Ord ( B i^i dom A ) ) )
18 dmres 
 |-  dom ( A |` B ) = ( B i^i dom A )
19 ordeq 
 |-  ( dom ( A |` B ) = ( B i^i dom A ) -> ( Ord dom ( A |` B ) <-> Ord ( B i^i dom A ) ) )
20 18 19 ax-mp 
 |-  ( Ord dom ( A |` B ) <-> Ord ( B i^i dom A ) )
21 17 20 imbitrrdi 
 |-  ( B e. dom A -> ( Ord dom A -> Ord dom ( A |` B ) ) )
22 dmresss 
 |-  dom ( A |` B ) C_ dom A
23 ssralv 
 |-  ( dom ( A |` B ) C_ dom A -> ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )
24 22 23 ax-mp 
 |-  ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) )
25 ssralv 
 |-  ( dom ( A |` B ) C_ dom A -> ( A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )
26 22 25 ax-mp 
 |-  ( A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) )
27 26 ralimi 
 |-  ( A. x e. dom ( A |` B ) A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) )
28 24 27 syl 
 |-  ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) )
29 resdmss 
 |-  dom ( A |` B ) C_ B
30 simpl 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> x e. dom ( A |` B ) )
31 29 30 sselid 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> x e. B )
32 31 fvresd 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( A |` B ) ` x ) = ( A ` x ) )
33 simpr 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> y e. dom ( A |` B ) )
34 29 33 sselid 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> y e. B )
35 34 fvresd 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( A |` B ) ` y ) = ( A ` y ) )
36 32 35 eleq12d 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) <-> ( A ` x ) e. ( A ` y ) ) )
37 36 imbi2d 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) <-> ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )
38 37 ralbidva 
 |-  ( x e. dom ( A |` B ) -> ( A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) <-> A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )
39 38 ralbiia 
 |-  ( A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) <-> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) )
40 28 39 sylibr 
 |-  ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) )
41 40 a1i 
 |-  ( B e. dom A -> ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) ) )
42 12 21 41 3anim123d 
 |-  ( B e. dom A -> ( ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) -> ( ( A |` B ) : dom ( A |` B ) --> On /\ Ord dom ( A |` B ) /\ A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) ) ) )
43 df-smo 
 |-  ( Smo A <-> ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )
44 df-smo 
 |-  ( Smo ( A |` B ) <-> ( ( A |` B ) : dom ( A |` B ) --> On /\ Ord dom ( A |` B ) /\ A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) ) )
45 42 43 44 3imtr4g 
 |-  ( B e. dom A -> ( Smo A -> Smo ( A |` B ) ) )
46 45 impcom 
 |-  ( ( Smo A /\ B e. dom A ) -> Smo ( A |` B ) )