Metamath Proof Explorer

Theorem smoel

Description: If x is less than y then a strictly monotone function's value will be strictly less at x than at y . (Contributed by Andrew Salmon, 22-Nov-2011)

Ref Expression
Assertion smoel 
|- ( ( Smo B /\ A e. dom B /\ C e. A ) -> ( B ` C ) e. ( B ` A ) )

Proof

Step Hyp Ref Expression
1 smodm 
 |-  ( Smo B -> Ord dom B )
2 ordtr1 
 |-  ( Ord dom B -> ( ( C e. A /\ A e. dom B ) -> C e. dom B ) )
3 2 ancomsd 
 |-  ( Ord dom B -> ( ( A e. dom B /\ C e. A ) -> C e. dom B ) )
4 3 expdimp 
 |-  ( ( Ord dom B /\ A e. dom B ) -> ( C e. A -> C e. dom B ) )
5 1 4 sylan 
 |-  ( ( Smo B /\ A e. dom B ) -> ( C e. A -> C e. dom B ) )
6 df-smo 
 |-  ( Smo B <-> ( B : dom B --> On /\ Ord dom B /\ A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) )
7 eleq1 
 |-  ( x = C -> ( x e. y <-> C e. y ) )
8 fveq2 
 |-  ( x = C -> ( B ` x ) = ( B ` C ) )
9 8 eleq1d 
 |-  ( x = C -> ( ( B ` x ) e. ( B ` y ) <-> ( B ` C ) e. ( B ` y ) ) )
10 7 9 imbi12d 
 |-  ( x = C -> ( ( x e. y -> ( B ` x ) e. ( B ` y ) ) <-> ( C e. y -> ( B ` C ) e. ( B ` y ) ) ) )
11 eleq2 
 |-  ( y = A -> ( C e. y <-> C e. A ) )
12 fveq2 
 |-  ( y = A -> ( B ` y ) = ( B ` A ) )
13 12 eleq2d 
 |-  ( y = A -> ( ( B ` C ) e. ( B ` y ) <-> ( B ` C ) e. ( B ` A ) ) )
14 11 13 imbi12d 
 |-  ( y = A -> ( ( C e. y -> ( B ` C ) e. ( B ` y ) ) <-> ( C e. A -> ( B ` C ) e. ( B ` A ) ) ) )
15 10 14 rspc2v 
 |-  ( ( C e. dom B /\ A e. dom B ) -> ( A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) -> ( C e. A -> ( B ` C ) e. ( B ` A ) ) ) )
16 15 ancoms 
 |-  ( ( A e. dom B /\ C e. dom B ) -> ( A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) -> ( C e. A -> ( B ` C ) e. ( B ` A ) ) ) )
17 16 com12 
 |-  ( A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) -> ( ( A e. dom B /\ C e. dom B ) -> ( C e. A -> ( B ` C ) e. ( B ` A ) ) ) )
18 17 3ad2ant3 
 |-  ( ( B : dom B --> On /\ Ord dom B /\ A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) -> ( ( A e. dom B /\ C e. dom B ) -> ( C e. A -> ( B ` C ) e. ( B ` A ) ) ) )
19 6 18 sylbi 
 |-  ( Smo B -> ( ( A e. dom B /\ C e. dom B ) -> ( C e. A -> ( B ` C ) e. ( B ` A ) ) ) )
20 19 expdimp 
 |-  ( ( Smo B /\ A e. dom B ) -> ( C e. dom B -> ( C e. A -> ( B ` C ) e. ( B ` A ) ) ) )
21 5 20 syld 
 |-  ( ( Smo B /\ A e. dom B ) -> ( C e. A -> ( C e. A -> ( B ` C ) e. ( B ` A ) ) ) )
22 21 pm2.43d 
 |-  ( ( Smo B /\ A e. dom B ) -> ( C e. A -> ( B ` C ) e. ( B ` A ) ) )
23 22 3impia 
 |-  ( ( Smo B /\ A e. dom B /\ C e. A ) -> ( B ` C ) e. ( B ` A ) )