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

Proof

Step	Hyp	Ref	Expression
1		df-le	$$⊢\le =\left({ℝ}^{*}\times {ℝ}^{*}\right)\setminus {<}^{-1}$$
2	1	ineq1i	$$⊢\le \cap \left(A\times A\right)=\left(\left({ℝ}^{*}\times {ℝ}^{*}\right)\setminus {<}^{-1}\right)\cap \left(A\times A\right)$$
3		indif1	$$⊢\left(\left({ℝ}^{*}\times {ℝ}^{*}\right)\setminus {<}^{-1}\right)\cap \left(A\times A\right)=\left(\left({ℝ}^{*}\times {ℝ}^{*}\right)\cap \left(A\times A\right)\right)\setminus {<}^{-1}$$
4	2 3	eqtri	$$⊢\le \cap \left(A\times A\right)=\left(\left({ℝ}^{*}\times {ℝ}^{*}\right)\cap \left(A\times A\right)\right)\setminus {<}^{-1}$$
5		xpss12	$$⊢\left(A\subseteq {ℝ}^{*}\wedge A\subseteq {ℝ}^{*}\right)\to A\times A\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
6	5	anidms	$$⊢A\subseteq {ℝ}^{*}\to A\times A\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
7		sseqin2	$$⊢A\times A\subseteq {ℝ}^{*}\times {ℝ}^{*}\leftrightarrow \left({ℝ}^{*}\times {ℝ}^{*}\right)\cap \left(A\times A\right)=A\times A$$
8	6 7	sylib	$$⊢A\subseteq {ℝ}^{*}\to \left({ℝ}^{*}\times {ℝ}^{*}\right)\cap \left(A\times A\right)=A\times A$$
9	8	difeq1d	$$⊢A\subseteq {ℝ}^{*}\to \left(\left({ℝ}^{*}\times {ℝ}^{*}\right)\cap \left(A\times A\right)\right)\setminus {<}^{-1}=\left(A\times A\right)\setminus {<}^{-1}$$
10	4 9	eqtr2id	$$⊢A\subseteq {ℝ}^{*}\to \left(A\times A\right)\setminus {<}^{-1}=\le \cap \left(A\times A\right)$$
11		isoeq2	$$⊢\left(A\times A\right)\setminus {<}^{-1}=\le \cap \left(A\times A\right)\to \left(F{Isom}_{\left(A\times A\right)\setminus {<}^{-1},\left(B\times B\right)\setminus {<}^{-1}}\left(A,B\right)\leftrightarrow F{Isom}_{\le \cap \left(A\times A\right),\left(B\times B\right)\setminus {<}^{-1}}\left(A,B\right)\right)$$
12	10 11	syl	$$⊢A\subseteq {ℝ}^{*}\to \left(F{Isom}_{\left(A\times A\right)\setminus {<}^{-1},\left(B\times B\right)\setminus {<}^{-1}}\left(A,B\right)\leftrightarrow F{Isom}_{\le \cap \left(A\times A\right),\left(B\times B\right)\setminus {<}^{-1}}\left(A,B\right)\right)$$
13	1	ineq1i	$$⊢\le \cap \left(B\times B\right)=\left(\left({ℝ}^{*}\times {ℝ}^{*}\right)\setminus {<}^{-1}\right)\cap \left(B\times B\right)$$
14		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}$$
15	13 14	eqtri	$$⊢\le \cap \left(B\times B\right)=\left(\left({ℝ}^{*}\times {ℝ}^{*}\right)\cap \left(B\times B\right)\right)\setminus {<}^{-1}$$
16		xpss12	$$⊢\left(B\subseteq {ℝ}^{*}\wedge B\subseteq {ℝ}^{*}\right)\to B\times B\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
17	16	anidms	$$⊢B\subseteq {ℝ}^{*}\to B\times B\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
18		sseqin2	$$⊢B\times B\subseteq {ℝ}^{*}\times {ℝ}^{*}\leftrightarrow \left({ℝ}^{*}\times {ℝ}^{*}\right)\cap \left(B\times B\right)=B\times B$$
19	17 18	sylib	$$⊢B\subseteq {ℝ}^{*}\to \left({ℝ}^{*}\times {ℝ}^{*}\right)\cap \left(B\times B\right)=B\times B$$
20	19	difeq1d	$$⊢B\subseteq {ℝ}^{*}\to \left(\left({ℝ}^{*}\times {ℝ}^{*}\right)\cap \left(B\times B\right)\right)\setminus {<}^{-1}=\left(B\times B\right)\setminus {<}^{-1}$$
21	15 20	eqtr2id	$$⊢B\subseteq {ℝ}^{*}\to \left(B\times B\right)\setminus {<}^{-1}=\le \cap \left(B\times B\right)$$
22		isoeq3	$$⊢\left(B\times B\right)\setminus {<}^{-1}=\le \cap \left(B\times B\right)\to \left(F{Isom}_{\le \cap \left(A\times A\right),\left(B\times B\right)\setminus {<}^{-1}}\left(A,B\right)\leftrightarrow F{Isom}_{\le \cap \left(A\times A\right),\le \cap \left(B\times B\right)}\left(A,B\right)\right)$$
23	21 22	syl	$$⊢B\subseteq {ℝ}^{*}\to \left(F{Isom}_{\le \cap \left(A\times A\right),\left(B\times B\right)\setminus {<}^{-1}}\left(A,B\right)\leftrightarrow F{Isom}_{\le \cap \left(A\times A\right),\le \cap \left(B\times B\right)}\left(A,B\right)\right)$$
24	12 23	sylan9bb	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\subseteq {ℝ}^{*}\right)\to \left(F{Isom}_{\left(A\times A\right)\setminus {<}^{-1},\left(B\times B\right)\setminus {<}^{-1}}\left(A,B\right)\leftrightarrow F{Isom}_{\le \cap \left(A\times A\right),\le \cap \left(B\times B\right)}\left(A,B\right)\right)$$
25		isocnv2	$$⊢F{Isom}_{<,<}\left(A,B\right)\leftrightarrow F{Isom}_{{<}^{-1},{<}^{-1}}\left(A,B\right)$$
26		eqid	$$⊢\left(A\times A\right)\setminus {<}^{-1}=\left(A\times A\right)\setminus {<}^{-1}$$
27		eqid	$$⊢\left(B\times B\right)\setminus {<}^{-1}=\left(B\times B\right)\setminus {<}^{-1}$$
28	26 27	isocnv3	$$⊢F{Isom}_{{<}^{-1},{<}^{-1}}\left(A,B\right)\leftrightarrow F{Isom}_{\left(A\times A\right)\setminus {<}^{-1},\left(B\times B\right)\setminus {<}^{-1}}\left(A,B\right)$$
29	25 28	bitri	$$⊢F{Isom}_{<,<}\left(A,B\right)\leftrightarrow F{Isom}_{\left(A\times A\right)\setminus {<}^{-1},\left(B\times B\right)\setminus {<}^{-1}}\left(A,B\right)$$
30		isores1	$$⊢F{Isom}_{\le ,\le }\left(A,B\right)\leftrightarrow F{Isom}_{\le \cap \left(A\times A\right),\le }\left(A,B\right)$$
31		isores2	$$⊢F{Isom}_{\le \cap \left(A\times A\right),\le }\left(A,B\right)\leftrightarrow F{Isom}_{\le \cap \left(A\times A\right),\le \cap \left(B\times B\right)}\left(A,B\right)$$
32	30 31	bitri	$$⊢F{Isom}_{\le ,\le }\left(A,B\right)\leftrightarrow F{Isom}_{\le \cap \left(A\times A\right),\le \cap \left(B\times B\right)}\left(A,B\right)$$
33	24 29 32	3bitr4g	$$⊢\left(A\subseteq {ℝ}^{*}\wedge B\subseteq {ℝ}^{*}\right)\to \left(F{Isom}_{<,<}\left(A,B\right)\leftrightarrow F{Isom}_{\le ,\le }\left(A,B\right)\right)$$