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 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {B}\subseteq {ℝ}^{*}\right)\to \left({F}{Isom}_{<,{<}^{-1}}\left({A},{B}\right)↔{F}{Isom}_{\le ,{\le }^{-1}}\left({A},{B}\right)\right)$

Proof

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