Metamath Proof Explorer

Theorem gtiso

Description: Two ways to write a strictly decreasing function on the reals. (Contributed by Thierry Arnoux, 6-Apr-2017)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ( A X. A ) \ < ) = ( ( A X. A ) \ < )
2 eqid 
 |-  ( ( B X. B ) \ `' < ) = ( ( B X. B ) \ `' < )
3 1 2 isocnv3 
 |-  ( F Isom < , `' < ( A , B ) <-> F Isom ( ( A X. A ) \ < ) , ( ( B X. B ) \ `' < ) ( A , B ) )
4 3 a1i 
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom < , `' < ( A , B ) <-> F Isom ( ( A X. A ) \ < ) , ( ( B X. B ) \ `' < ) ( A , B ) ) )
5 df-le 
 |-  <_ = ( ( RR* X. RR* ) \ `' < )
6 5 cnveqi 
 |-  `' <_ = `' ( ( RR* X. RR* ) \ `' < )
7 cnvdif 
 |-  `' ( ( RR* X. RR* ) \ `' < ) = ( `' ( RR* X. RR* ) \ `' `' < )
8 cnvxp 
 |-  `' ( RR* X. RR* ) = ( RR* X. RR* )
9 ltrel 
 |-  Rel <
10 dfrel2 
 |-  ( Rel < <-> `' `' < = < )
11 9 10 mpbi 
 |-  `' `' < = <
12 8 11 difeq12i 
 |-  ( `' ( RR* X. RR* ) \ `' `' < ) = ( ( RR* X. RR* ) \ < )
13 6 7 12 3eqtri 
 |-  `' <_ = ( ( RR* X. RR* ) \ < )
14 13 ineq1i 
 |-  ( `' <_ i^i ( A X. A ) ) = ( ( ( RR* X. RR* ) \ < ) i^i ( A X. A ) )
15 indif1 
 |-  ( ( ( RR* X. RR* ) \ < ) i^i ( A X. A ) ) = ( ( ( RR* X. RR* ) i^i ( A X. A ) ) \ < )
16 14 15 eqtri 
 |-  ( `' <_ i^i ( A X. A ) ) = ( ( ( RR* X. RR* ) i^i ( A X. A ) ) \ < )
17 xpss12 
 |-  ( ( A C_ RR* /\ A C_ RR* ) -> ( A X. A ) C_ ( RR* X. RR* ) )
18 17 anidms 
 |-  ( A C_ RR* -> ( A X. A ) C_ ( RR* X. RR* ) )
19 sseqin2 
 |-  ( ( A X. A ) C_ ( RR* X. RR* ) <-> ( ( RR* X. RR* ) i^i ( A X. A ) ) = ( A X. A ) )
20 18 19 sylib 
 |-  ( A C_ RR* -> ( ( RR* X. RR* ) i^i ( A X. A ) ) = ( A X. A ) )
21 20 difeq1d 
 |-  ( A C_ RR* -> ( ( ( RR* X. RR* ) i^i ( A X. A ) ) \ < ) = ( ( A X. A ) \ < ) )
22 16 21 eqtr2id 
 |-  ( A C_ RR* -> ( ( A X. A ) \ < ) = ( `' <_ i^i ( A X. A ) ) )
23 22 adantr 
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( ( A X. A ) \ < ) = ( `' <_ i^i ( A X. A ) ) )
24 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 ) ) )
25 23 24 syl 
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom ( ( A X. A ) \ < ) , ( ( B X. B ) \ `' < ) ( A , B ) <-> F Isom ( `' <_ i^i ( A X. A ) ) , ( ( B X. B ) \ `' < ) ( A , B ) ) )
26 5 ineq1i 
 |-  ( <_ i^i ( B X. B ) ) = ( ( ( RR* X. RR* ) \ `' < ) i^i ( B X. B ) )
27 indif1 
 |-  ( ( ( RR* X. RR* ) \ `' < ) i^i ( B X. B ) ) = ( ( ( RR* X. RR* ) i^i ( B X. B ) ) \ `' < )
28 26 27 eqtri 
 |-  ( <_ i^i ( B X. B ) ) = ( ( ( RR* X. RR* ) i^i ( B X. B ) ) \ `' < )
29 xpss12 
 |-  ( ( B C_ RR* /\ B C_ RR* ) -> ( B X. B ) C_ ( RR* X. RR* ) )
30 29 anidms 
 |-  ( B C_ RR* -> ( B X. B ) C_ ( RR* X. RR* ) )
31 sseqin2 
 |-  ( ( B X. B ) C_ ( RR* X. RR* ) <-> ( ( RR* X. RR* ) i^i ( B X. B ) ) = ( B X. B ) )
32 30 31 sylib 
 |-  ( B C_ RR* -> ( ( RR* X. RR* ) i^i ( B X. B ) ) = ( B X. B ) )
33 32 difeq1d 
 |-  ( B C_ RR* -> ( ( ( RR* X. RR* ) i^i ( B X. B ) ) \ `' < ) = ( ( B X. B ) \ `' < ) )
34 28 33 eqtr2id 
 |-  ( B C_ RR* -> ( ( B X. B ) \ `' < ) = ( <_ i^i ( B X. B ) ) )
35 34 adantl 
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( ( B X. B ) \ `' < ) = ( <_ i^i ( B X. B ) ) )
36 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 ) ) )
37 35 36 syl 
 |-  ( ( A C_ RR* /\ 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 ) ) )
38 4 25 37 3bitrd 
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom < , `' < ( A , B ) <-> F Isom ( `' <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) ) )
39 isocnv2 
 |-  ( F Isom `' <_ , <_ ( A , B ) <-> F Isom `' `' <_ , `' <_ ( A , B ) )
40 isores2 
 |-  ( F Isom `' <_ , <_ ( A , B ) <-> F Isom `' <_ , ( <_ i^i ( B X. B ) ) ( A , B ) )
41 isores1 
 |-  ( F Isom `' <_ , ( <_ i^i ( B X. B ) ) ( A , B ) <-> F Isom ( `' <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) )
42 40 41 bitri 
 |-  ( F Isom `' <_ , <_ ( A , B ) <-> F Isom ( `' <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) )
43 lerel 
 |-  Rel <_
44 dfrel2 
 |-  ( Rel <_ <-> `' `' <_ = <_ )
45 43 44 mpbi 
 |-  `' `' <_ = <_
46 isoeq2 
 |-  ( `' `' <_ = <_ -> ( F Isom `' `' <_ , `' <_ ( A , B ) <-> F Isom <_ , `' <_ ( A , B ) ) )
47 45 46 ax-mp 
 |-  ( F Isom `' `' <_ , `' <_ ( A , B ) <-> F Isom <_ , `' <_ ( A , B ) )
48 39 42 47 3bitr3ri 
 |-  ( F Isom <_ , `' <_ ( A , B ) <-> F Isom ( `' <_ i^i ( A X. A ) ) , ( <_ i^i ( B X. B ) ) ( A , B ) )
49 38 48 bitr4di 
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( F Isom < , `' < ( A , B ) <-> F Isom <_ , `' <_ ( A , B ) ) )