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 x dom F y x F y 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 ran F
9 7 8 eqsstrri ran F A ran F
10 2 frnd Smo F ran F On
11 9 10 sstrid Smo F ran F A On
12 df-f F A : dom F A On F A Fn dom F A ran F A 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 dom F
17 dmres dom F A = A dom F
18 ordeq dom F A = A dom F Ord dom F A Ord A dom F
19 17 18 ax-mp Ord dom F A Ord A 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 F
24 dmss F A F dom F A dom F
25 23 24 ax-mp dom F A dom F
26 1 simp3bi Smo F x dom F y x F y F x
27 ssralv dom F A dom F x dom F y x F y F x x dom F A y x F y F x
28 25 26 27 mpsyl Smo F x dom F A y x F y F x
29 28 adantr Smo F Ord A x dom F A y x F y F x
30 ordtr1 Ord dom F A y x x dom F A y dom F A
31 22 30 syl Smo F Ord A y x x dom F A y dom F A
32 inss1 A dom F A
33 17 32 eqsstri dom F A A
34 33 sseli y dom F A y A
35 31 34 syl6 Smo F Ord A y x x dom F A y A
36 35 expcomd Smo F Ord A x dom F A y x y A
37 36 imp31 Smo F Ord A x dom F A y x y A
38 37 fvresd Smo F Ord A x dom F A y x F A y = F y
39 33 sseli x dom F A x A
40 39 fvresd x dom F A F A x = F x
41 40 ad2antlr Smo F Ord A x dom F A y x F A x = F x
42 38 41 eleq12d Smo F Ord A x dom F A y x F A y F A x F y F x
43 42 ralbidva Smo F Ord A x dom F A y x F A y F A x y x F y F x
44 43 ralbidva Smo F Ord A x dom F A y x F A y F A x x dom F A y x F y F x
45 29 44 mpbird Smo F Ord A x dom F A y x F A y F A x
46 dfsmo2 Smo F A F A : dom F A On Ord dom F A x dom F A y x F A y F A x
47 14 22 45 46 syl3anbrc Smo F Ord A Smo F A