Metamath Proof Explorer

Theorem leisorel

Description: Version of isorel for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015) (Revised by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion leisorel 
|- ( ( F Isom < , < ( A , B ) /\ ( A C_ RR* /\ B C_ RR* ) /\ ( C e. A /\ D e. A ) ) -> ( C <_ D <-> ( F ` C ) <_ ( F ` D ) ) )

Proof

Step Hyp Ref Expression
1 leiso 
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom < , < ( A , B ) <-> F Isom <_ , <_ ( A , B ) ) )
2 1 biimpcd 
 |-  ( F Isom < , < ( A , B ) -> ( ( A C_ RR* /\ B C_ RR* ) -> F Isom <_ , <_ ( A , B ) ) )
3 isorel 
 |-  ( ( F Isom <_ , <_ ( A , B ) /\ ( C e. A /\ D e. A ) ) -> ( C <_ D <-> ( F ` C ) <_ ( F ` D ) ) )
4 3 ex 
 |-  ( F Isom <_ , <_ ( A , B ) -> ( ( C e. A /\ D e. A ) -> ( C <_ D <-> ( F ` C ) <_ ( F ` D ) ) ) )
5 2 4 syl6 
 |-  ( F Isom < , < ( A , B ) -> ( ( A C_ RR* /\ B C_ RR* ) -> ( ( C e. A /\ D e. A ) -> ( C <_ D <-> ( F ` C ) <_ ( F ` D ) ) ) ) )
6 5 3imp 
 |-  ( ( F Isom < , < ( A , B ) /\ ( A C_ RR* /\ B C_ RR* ) /\ ( C e. A /\ D e. A ) ) -> ( C <_ D <-> ( F ` C ) <_ ( F ` D ) ) )