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 resss 
 |-  ( A |` B ) C_ A
6 5 rnssi 
 |-  ran ( A |` B ) C_ ran A
7 sstr 
 |-  ( ( ran ( A |` B ) C_ ran A /\ ran A C_ On ) -> ran ( A |` B ) C_ On )
8 6 7 mpan 
 |-  ( ran A C_ On -> ran ( A |` B ) C_ On )
9 4 8 anim12i 
 |-  ( ( A Fn dom A /\ ran A C_ On ) -> ( ( A |` B ) Fn dom ( A |` B ) /\ ran ( A |` B ) C_ On ) )
10 df-f 
 |-  ( A : dom A --> On <-> ( A Fn dom A /\ ran A C_ On ) )
11 df-f 
 |-  ( ( A |` B ) : dom ( A |` B ) --> On <-> ( ( A |` B ) Fn dom ( A |` B ) /\ ran ( A |` B ) C_ On ) )
12 9 10 11 3imtr4i 
 |-  ( A : dom A --> On -> ( A |` B ) : dom ( A |` B ) --> On )
13 12 a1i 
 |-  ( B e. dom A -> ( A : dom A --> On -> ( A |` B ) : dom ( A |` B ) --> On ) )
14 ordelord 
 |-  ( ( Ord dom A /\ B e. dom A ) -> Ord B )
15 14 expcom 
 |-  ( B e. dom A -> ( Ord dom A -> Ord B ) )
16 ordin 
 |-  ( ( Ord B /\ Ord dom A ) -> Ord ( B i^i dom A ) )
17 16 ex 
 |-  ( Ord B -> ( Ord dom A -> Ord ( B i^i dom A ) ) )
18 15 17 syli 
 |-  ( B e. dom A -> ( Ord dom A -> Ord ( B i^i dom A ) ) )
19 dmres 
 |-  dom ( A |` B ) = ( B i^i dom A )
20 ordeq 
 |-  ( dom ( A |` B ) = ( B i^i dom A ) -> ( Ord dom ( A |` B ) <-> Ord ( B i^i dom A ) ) )
21 19 20 ax-mp 
 |-  ( Ord dom ( A |` B ) <-> Ord ( B i^i dom A ) )
22 18 21 imbitrrdi 
 |-  ( B e. dom A -> ( Ord dom A -> Ord dom ( A |` B ) ) )
23 dmss 
 |-  ( ( A |` B ) C_ A -> dom ( A |` B ) C_ dom A )
24 5 23 ax-mp 
 |-  dom ( A |` B ) C_ dom A
25 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 ) ) ) )
26 24 25 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 ) ) )
27 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 ) ) ) )
28 24 27 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 ) ) )
29 28 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 ) ) )
30 26 29 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 ) ) )
31 inss1 
 |-  ( B i^i dom A ) C_ B
32 19 31 eqsstri 
 |-  dom ( A |` B ) C_ B
33 simpl 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> x e. dom ( A |` B ) )
34 32 33 sselid 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> x e. B )
35 34 fvresd 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( A |` B ) ` x ) = ( A ` x ) )
36 simpr 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> y e. dom ( A |` B ) )
37 32 36 sselid 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> y e. B )
38 37 fvresd 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( A |` B ) ` y ) = ( A ` y ) )
39 35 38 eleq12d 
 |-  ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) <-> ( A ` x ) e. ( A ` y ) ) )
40 39 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 ) ) ) )
41 40 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 ) ) ) )
42 41 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 ) ) )
43 30 42 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 ) ) )
44 43 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 ) ) ) )
45 13 22 44 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 ) ) ) ) )
46 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 ) ) ) )
47 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 ) ) ) )
48 45 46 47 3imtr4g 
 |-  ( B e. dom A -> ( Smo A -> Smo ( A |` B ) ) )
49 48 impcom 
 |-  ( ( Smo A /\ B e. dom A ) -> Smo ( A |` B ) )