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)\leftrightarrow F{Isom}_{\le ,{\le }^{-1}}\left(A,B\right)\right)$$

Proof

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