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