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