This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( dom A i^i B ) /\ Ord B ) -> Smo ( A |` C ) )

Proof

Step Hyp Ref Expression
1 dmres 
 |-  dom ( A |` B ) = ( B i^i dom A )
2 incom 
 |-  ( B i^i dom A ) = ( dom A i^i B )
3 1 2 eqtri 
 |-  dom ( A |` B ) = ( dom A i^i B )
4 3 eleq2i 
 |-  ( C e. dom ( A |` B ) <-> C e. ( dom A i^i B ) )
5 smores 
 |-  ( ( Smo ( A |` B ) /\ C e. dom ( A |` B ) ) -> Smo ( ( A |` B ) |` C ) )
6 4 5 sylan2br 
 |-  ( ( Smo ( A |` B ) /\ C e. ( dom A i^i B ) ) -> Smo ( ( A |` B ) |` C ) )
7 6 3adant3 
 |-  ( ( Smo ( A |` B ) /\ C e. ( dom A i^i B ) /\ Ord B ) -> Smo ( ( A |` B ) |` C ) )
8 elinel2 
 |-  ( C e. ( dom A i^i B ) -> C e. B )
9 ordelss 
 |-  ( ( Ord B /\ C e. B ) -> C C_ B )
10 9 ancoms 
 |-  ( ( C e. B /\ Ord B ) -> C C_ B )
11 8 10 sylan 
 |-  ( ( C e. ( dom A i^i B ) /\ Ord B ) -> C C_ B )
12 11 3adant1 
 |-  ( ( Smo ( A |` B ) /\ C e. ( dom A i^i B ) /\ Ord B ) -> C C_ B )
13 resabs1 
 |-  ( C 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 e. ( dom A i^i B ) /\ Ord B ) -> ( Smo ( ( A |` B ) |` C ) <-> Smo ( A |` C ) ) )
16 7 15 mpbid 
 |-  ( ( Smo ( A |` B ) /\ C e. ( dom A i^i B ) /\ Ord B ) -> Smo ( A |` C ) )