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 * B * F Isom < , < -1 A B F Isom , -1 A B

Proof

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