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