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