Metamath Proof Explorer


Theorem smores3

Description: A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion smores3 Smo A B C dom A B Ord B Smo A C

Proof

Step Hyp Ref Expression
1 dmres dom A B = B dom A
2 incom B dom A = dom A B
3 1 2 eqtri dom A B = dom A B
4 3 eleq2i C dom A B C dom A B
5 smores Smo A B C dom A B Smo A B C
6 4 5 sylan2br Smo A B C dom A B Smo A B C
7 6 3adant3 Smo A B C dom A B Ord B Smo A B C
8 elinel2 C dom A B C B
9 ordelss Ord B C B C B
10 9 ancoms C B Ord B C B
11 8 10 sylan C dom A B Ord B C B
12 11 3adant1 Smo A B C dom A B Ord B C B
13 resabs1 C B A B C = A C
14 smoeq A B C = A C Smo A B C Smo A C
15 12 13 14 3syl Smo A B C dom A B Ord B Smo A B C Smo A C
16 7 15 mpbid Smo A B C dom A B Ord B Smo A C