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 SmoBAdomBCABCBA

Proof

Step Hyp Ref Expression
1 smodm SmoBOrddomB
2 ordtr1 OrddomBCAAdomBCdomB
3 2 ancomsd OrddomBAdomBCACdomB
4 3 expdimp OrddomBAdomBCACdomB
5 1 4 sylan SmoBAdomBCACdomB
6 df-smo SmoBB:domBOnOrddomBxdomBydomBxyBxBy
7 eleq1 x=CxyCy
8 fveq2 x=CBx=BC
9 8 eleq1d x=CBxByBCBy
10 7 9 imbi12d x=CxyBxByCyBCBy
11 eleq2 y=ACyCA
12 fveq2 y=ABy=BA
13 12 eleq2d y=ABCByBCBA
14 11 13 imbi12d y=ACyBCByCABCBA
15 10 14 rspc2v CdomBAdomBxdomBydomBxyBxByCABCBA
16 15 ancoms AdomBCdomBxdomBydomBxyBxByCABCBA
17 16 com12 xdomBydomBxyBxByAdomBCdomBCABCBA
18 17 3ad2ant3 B:domBOnOrddomBxdomBydomBxyBxByAdomBCdomBCABCBA
19 6 18 sylbi SmoBAdomBCdomBCABCBA
20 19 expdimp SmoBAdomBCdomBCABCBA
21 5 20 syld SmoBAdomBCACABCBA
22 21 pm2.43d SmoBAdomBCABCBA
23 22 3impia SmoBAdomBCABCBA