Metamath Proof Explorer


Theorem leiso

Description: Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion leiso
|- ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom < , < ( A , B ) <-> F Isom <_ , <_ ( A , B ) ) )

Proof

Step Hyp Ref Expression
1 df-le
 |-  <_ = ( ( RR* X. RR* ) \ `' < )
2 1 ineq1i
 |-  ( <_ i^i ( A X. A ) ) = ( ( ( RR* X. RR* ) \ `' < ) i^i ( A X. A ) )
3 indif1
 |-  ( ( ( RR* X. RR* ) \ `' < ) i^i ( A X. A ) ) = ( ( ( RR* X. RR* ) i^i ( A X. A ) ) \ `' < )
4 2 3 eqtri
 |-  ( <_ i^i ( A X. A ) ) = ( ( ( RR* X. RR* ) i^i ( A X. A ) ) \ `' < )
5 xpss12
 |-  ( ( A C_ RR* /\ A C_ RR* ) -> ( A X. A ) C_ ( RR* X. RR* ) )
6 5 anidms
 |-  ( A C_ RR* -> ( A X. A ) C_ ( RR* X. RR* ) )
7 sseqin2
 |-  ( ( A X. A ) C_ ( RR* X. RR* ) <-> ( ( RR* X. RR* ) i^i ( A X. A ) ) = ( A X. A ) )
8 6 7 sylib
 |-  ( A C_ RR* -> ( ( RR* X. RR* ) i^i ( A X. A ) ) = ( A X. A ) )
9 8 difeq1d
 |-  ( A C_ RR* -> ( ( ( RR* X. RR* ) i^i ( A X. A ) ) \ `' < ) = ( ( A X. A ) \ `' < ) )
10 4 9 eqtr2id
 |-  ( A C_ RR* -> ( ( A X. A ) \ `' < ) = ( <_ i^i ( A X. A ) ) )
11 isoeq2
 |-  ( ( ( A X. A ) \ `' < ) = ( <_ i^i ( A X. A ) ) -> ( F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( ( B X. B ) \ `' < ) ( A , B ) ) )
12 10 11 syl
 |-  ( A C_ RR* -> ( F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( ( B X. B ) \ `' < ) ( A , B ) ) )
13 1 ineq1i
 |-  ( <_ i^i ( B X. B ) ) = ( ( ( RR* X. RR* ) \ `' < ) i^i ( B X. B ) )
14 indif1
 |-  ( ( ( RR* X. RR* ) \ `' < ) i^i ( B X. B ) ) = ( ( ( RR* X. RR* ) i^i ( B X. B ) ) \ `' < )
15 13 14 eqtri
 |-  ( <_ i^i ( B X. B ) ) = ( ( ( RR* X. RR* ) i^i ( B X. B ) ) \ `' < )
16 xpss12
 |-  ( ( B C_ RR* /\ B C_ RR* ) -> ( B X. B ) C_ ( RR* X. RR* ) )
17 16 anidms
 |-  ( B C_ RR* -> ( B X. B ) C_ ( RR* X. RR* ) )
18 sseqin2
 |-  ( ( B X. B ) C_ ( RR* X. RR* ) <-> ( ( RR* X. RR* ) i^i ( B X. B ) ) = ( B X. B ) )
19 17 18 sylib
 |-  ( B C_ RR* -> ( ( RR* X. RR* ) i^i ( B X. B ) ) = ( B X. B ) )
20 19 difeq1d
 |-  ( B C_ RR* -> ( ( ( RR* X. RR* ) i^i ( B X. B ) ) \ `' < ) = ( ( B X. B ) \ `' < ) )
21 15 20 eqtr2id
 |-  ( B C_ RR* -> ( ( B X. B ) \ `' < ) = ( <_ i^i ( B X. B ) ) )
22 isoeq3
 |-  ( ( ( B X. B ) \ `' < ) = ( <_ i^i ( B X. B ) ) -> ( F Isom ( <_ i^i ( A X. A ) ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) ) )
23 21 22 syl
 |-  ( B C_ RR* -> ( F Isom ( <_ i^i ( A X. A ) ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) ) )
24 12 23 sylan9bb
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) ) )
25 isocnv2
 |-  ( F Isom < , < ( A , B ) <-> F Isom `' < , `' < ( A , B ) )
26 eqid
 |-  ( ( A X. A ) \ `' < ) = ( ( A X. A ) \ `' < )
27 eqid
 |-  ( ( B X. B ) \ `' < ) = ( ( B X. B ) \ `' < )
28 26 27 isocnv3
 |-  ( F Isom `' < , `' < ( A , B ) <-> F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) )
29 25 28 bitri
 |-  ( F Isom < , < ( A , B ) <-> F Isom ( ( A X. A ) \ `' < ) , ( ( B X. B ) \ `' < ) ( A , B ) )
30 isores1
 |-  ( F Isom <_ , <_ ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , <_ ( A , B ) )
31 isores2
 |-  ( F Isom ( <_ i^i ( A X. A ) ) , <_ ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) )
32 30 31 bitri
 |-  ( F Isom <_ , <_ ( A , B ) <-> F Isom ( <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) )
33 24 29 32 3bitr4g
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom < , < ( A , B ) <-> F Isom <_ , <_ ( A , B ) ) )