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