xrhmeo

Description: The bijection from [ -u 1 , 1 ] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Hypotheses	xrhmeo.f	$⊢ F = (x \in [0, 1] ⟼ if (x = 1, +∞, \frac{x}{1 - x}))$
	xrhmeo.g	$⊢ G = (y \in [- 1, 1] ⟼ if (0 \leq y, F (y), - F (- y)))$
	xrhmeo.j	$⊢ J = TopOpen (ℂ_{fld})$
Assertion	xrhmeo	$⊢ (G {Isom}_{<, <} ([- 1, 1], ℝ^{*}) \land G \in ((J ↾_{𝑡} [- 1, 1]) Homeo ordTop (\leq)))$

Proof

Step	Hyp	Ref	Expression
1		xrhmeo.f	$⊢ F = (x \in [0, 1] ⟼ if (x = 1, +∞, \frac{x}{1 - x}))$
2		xrhmeo.g	$⊢ G = (y \in [- 1, 1] ⟼ if (0 \leq y, F (y), - F (- y)))$
3		xrhmeo.j	$⊢ J = TopOpen (ℂ_{fld})$
4		iccssxr	$⊢ [- 1, 1] \subseteq ℝ^{*}$
5		xrltso	$⊢ < Or ℝ^{*}$
6		soss	$⊢ [- 1, 1] \subseteq ℝ^{} \to (< Or ℝ^{} \to < Or [- 1, 1])$
7	4 5 6	mp2	$⊢ < Or [- 1, 1]$
8		sopo	$⊢ < Or ℝ^{} \to < Po ℝ^{}$
9	5 8	ax-mp	$⊢ < Po ℝ^{*}$
10		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
11		neg1rr	$⊢ - 1 \in ℝ$
12		1re	$⊢ 1 \in ℝ$
13	11 12	elicc2i	$⊢ y \in [- 1, 1] \leftrightarrow (y \in ℝ \land - 1 \leq y \land y \leq 1)$
14	13	simp1bi	$⊢ y \in [- 1, 1] \to y \in ℝ$
15	14	adantr	$⊢ (y \in [- 1, 1] \land 0 \leq y) \to y \in ℝ$
16		simpr	$⊢ (y \in [- 1, 1] \land 0 \leq y) \to 0 \leq y$
17	13	simp3bi	$⊢ y \in [- 1, 1] \to y \leq 1$
18	17	adantr	$⊢ (y \in [- 1, 1] \land 0 \leq y) \to y \leq 1$
19		elicc01	$⊢ y \in [0, 1] \leftrightarrow (y \in ℝ \land 0 \leq y \land y \leq 1)$
20	15 16 18 19	syl3anbrc	$⊢ (y \in [- 1, 1] \land 0 \leq y) \to y \in [0, 1]$
21	1	iccpnfcnv	$⊢ (F : [0, 1] \underset{1-1 onto}{⟶} [0, +∞] \land F^{-1} = (v \in [0, +∞] ⟼ if (v = +∞, 1, \frac{v}{1 + v})))$
22	21	simpli	$⊢ F : [0, 1] \underset{1-1 onto}{⟶} [0, +∞]$
23		f1of	$⊢ F : [0, 1] \underset{1-1 onto}{⟶} [0, +∞] \to F : [0, 1] ⟶ [0, +∞]$
24	22 23	ax-mp	$⊢ F : [0, 1] ⟶ [0, +∞]$
25	24	ffvelrni	$⊢ y \in [0, 1] \to F (y) \in [0, +∞]$
26	20 25	syl	$⊢ (y \in [- 1, 1] \land 0 \leq y) \to F (y) \in [0, +∞]$
27	10 26	sselid	$⊢ (y \in [- 1, 1] \land 0 \leq y) \to F (y) \in ℝ^{*}$
28	14	adantr	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to y \in ℝ$
29	28	renegcld	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to - y \in ℝ$
30		0re	$⊢ 0 \in ℝ$
31		letric	$⊢ (0 \in ℝ \land y \in ℝ) \to (0 \leq y \lor y \leq 0)$
32	30 14 31	sylancr	$⊢ y \in [- 1, 1] \to (0 \leq y \lor y \leq 0)$
33	32	orcanai	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to y \leq 0$
34	28	le0neg1d	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to (y \leq 0 \leftrightarrow 0 \leq - y)$
35	33 34	mpbid	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to 0 \leq - y$
36	13	simp2bi	$⊢ y \in [- 1, 1] \to - 1 \leq y$
37	36	adantr	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to - 1 \leq y$
38		lenegcon1	$⊢ (1 \in ℝ \land y \in ℝ) \to (- 1 \leq y \leftrightarrow - y \leq 1)$
39	12 28 38	sylancr	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to (- 1 \leq y \leftrightarrow - y \leq 1)$
40	37 39	mpbid	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to - y \leq 1$
41		elicc01	$⊢ - y \in [0, 1] \leftrightarrow (- y \in ℝ \land 0 \leq - y \land - y \leq 1)$
42	29 35 40 41	syl3anbrc	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to - y \in [0, 1]$
43	24	ffvelrni	$⊢ - y \in [0, 1] \to F (- y) \in [0, +∞]$
44	42 43	syl	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to F (- y) \in [0, +∞]$
45	10 44	sselid	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to F (- y) \in ℝ^{*}$
46	45	xnegcld	$⊢ (y \in [- 1, 1] \land \neg 0 \leq y) \to - F (- y) \in ℝ^{*}$
47	27 46	ifclda	$⊢ y \in [- 1, 1] \to if (0 \leq y, F (y), - F (- y)) \in ℝ^{*}$
48	2 47	fmpti	$⊢ G : [- 1, 1] ⟶ ℝ^{*}$
49		frn	$⊢ G : [- 1, 1] ⟶ ℝ^{} \to ran G \subseteq ℝ^{}$
50	48 49	ax-mp	$⊢ ran G \subseteq ℝ^{*}$
51		ssabral	$⊢ ℝ^{} \subseteq \{z \| \exists y \in [- 1, 1] z = if (0 \leq y, F (y), - F (- y))\} \leftrightarrow \forall z \in ℝ^{} \exists y \in [- 1, 1] z = if (0 \leq y, F (y), - F (- y))$
52		0le1	$⊢ 0 \leq 1$
53		le0neg2	$⊢ 1 \in ℝ \to (0 \leq 1 \leftrightarrow - 1 \leq 0)$
54	12 53	ax-mp	$⊢ 0 \leq 1 \leftrightarrow - 1 \leq 0$
55	52 54	mpbi	$⊢ - 1 \leq 0$
56		1le1	$⊢ 1 \leq 1$
57		iccss	$⊢ ((- 1 \in ℝ \land 1 \in ℝ) \land (- 1 \leq 0 \land 1 \leq 1)) \to [0, 1] \subseteq [- 1, 1]$
58	11 12 55 56 57	mp4an	$⊢ [0, 1] \subseteq [- 1, 1]$
59		elxrge0	$⊢ z \in [0, +∞] \leftrightarrow (z \in ℝ^{*} \land 0 \leq z)$
60		f1ocnv	$⊢ F : [0, 1] \underset{1-1 onto}{⟶} [0, +∞] \to F^{-1} : [0, +∞] \underset{1-1 onto}{⟶} [0, 1]$
61		f1of	$⊢ F^{-1} : [0, +∞] \underset{1-1 onto}{⟶} [0, 1] \to F^{-1} : [0, +∞] ⟶ [0, 1]$
62	22 60 61	mp2b	$⊢ F^{-1} : [0, +∞] ⟶ [0, 1]$
63	62	ffvelrni	$⊢ z \in [0, +∞] \to F^{-1} (z) \in [0, 1]$
64	59 63	sylbir	$⊢ (z \in ℝ^{*} \land 0 \leq z) \to F^{-1} (z) \in [0, 1]$
65	58 64	sselid	$⊢ (z \in ℝ^{*} \land 0 \leq z) \to F^{-1} (z) \in [- 1, 1]$
66		elicc01	$⊢ F^{-1} (z) \in [0, 1] \leftrightarrow (F^{-1} (z) \in ℝ \land 0 \leq F^{-1} (z) \land F^{-1} (z) \leq 1)$
67	66	simp2bi	$⊢ F^{-1} (z) \in [0, 1] \to 0 \leq F^{-1} (z)$
68	64 67	syl	$⊢ (z \in ℝ^{*} \land 0 \leq z) \to 0 \leq F^{-1} (z)$
69	59	biimpri	$⊢ (z \in ℝ^{*} \land 0 \leq z) \to z \in [0, +∞]$
70		f1ocnvfv2	$⊢ (F : [0, 1] \underset{1-1 onto}{⟶} [0, +∞] \land z \in [0, +∞]) \to F (F^{-1} (z)) = z$
71	22 69 70	sylancr	$⊢ (z \in ℝ^{*} \land 0 \leq z) \to F (F^{-1} (z)) = z$
72	71	eqcomd	$⊢ (z \in ℝ^{*} \land 0 \leq z) \to z = F (F^{-1} (z))$
73		breq2	$⊢ y = F^{-1} (z) \to (0 \leq y \leftrightarrow 0 \leq F^{-1} (z))$
74		fveq2	$⊢ y = F^{-1} (z) \to F (y) = F (F^{-1} (z))$
75	74	eqeq2d	$⊢ y = F^{-1} (z) \to (z = F (y) \leftrightarrow z = F (F^{-1} (z)))$
76	73 75	anbi12d	$⊢ y = F^{-1} (z) \to ((0 \leq y \land z = F (y)) \leftrightarrow (0 \leq F^{-1} (z) \land z = F (F^{-1} (z))))$
77	76	rspcev	$⊢ (F^{-1} (z) \in [- 1, 1] \land (0 \leq F^{-1} (z) \land z = F (F^{-1} (z)))) \to \exists y \in [- 1, 1] (0 \leq y \land z = F (y))$
78	65 68 72 77	syl12anc	$⊢ (z \in ℝ^{*} \land 0 \leq z) \to \exists y \in [- 1, 1] (0 \leq y \land z = F (y))$
79		iftrue	$⊢ 0 \leq y \to if (0 \leq y, F (y), - F (- y)) = F (y)$
80	79	eqeq2d	$⊢ 0 \leq y \to (z = if (0 \leq y, F (y), - F (- y)) \leftrightarrow z = F (y))$
81	80	biimpar	$⊢ (0 \leq y \land z = F (y)) \to z = if (0 \leq y, F (y), - F (- y))$
82	81	reximi	$⊢ \exists y \in [- 1, 1] (0 \leq y \land z = F (y)) \to \exists y \in [- 1, 1] z = if (0 \leq y, F (y), - F (- y))$
83	78 82	syl	$⊢ (z \in ℝ^{*} \land 0 \leq z) \to \exists y \in [- 1, 1] z = if (0 \leq y, F (y), - F (- y))$
84		xnegcl	$⊢ z \in ℝ^{} \to - z \in ℝ^{}$
85	84	adantr	$⊢ (z \in ℝ^{} \land \neg 0 \leq z) \to - z \in ℝ^{}$
86		0xr	$⊢ 0 \in ℝ^{*}$
87		xrletri	$⊢ (0 \in ℝ^{} \land z \in ℝ^{}) \to (0 \leq z \lor z \leq 0)$
88	86 87	mpan	$⊢ z \in ℝ^{*} \to (0 \leq z \lor z \leq 0)$
89	88	ord	$⊢ z \in ℝ^{*} \to (\neg 0 \leq z \to z \leq 0)$
90		xle0neg1	$⊢ z \in ℝ^{*} \to (z \leq 0 \leftrightarrow 0 \leq - z)$
91	89 90	sylibd	$⊢ z \in ℝ^{*} \to (\neg 0 \leq z \to 0 \leq - z)$
92	91	imp	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to 0 \leq - z$
93		elxrge0	$⊢ - z \in [0, +∞] \leftrightarrow (- z \in ℝ^{*} \land 0 \leq - z)$
94	85 92 93	sylanbrc	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to - z \in [0, +∞]$
95	62	ffvelrni	$⊢ - z \in [0, +∞] \to F^{-1} (- z) \in [0, 1]$
96	94 95	syl	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to F^{-1} (- z) \in [0, 1]$
97	58 96	sselid	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to F^{-1} (- z) \in [- 1, 1]$
98		iccssre	$⊢ (- 1 \in ℝ \land 1 \in ℝ) \to [- 1, 1] \subseteq ℝ$
99	11 12 98	mp2an	$⊢ [- 1, 1] \subseteq ℝ$
100	99 97	sselid	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to F^{-1} (- z) \in ℝ$
101		iccneg	$⊢ (- 1 \in ℝ \land 1 \in ℝ \land F^{-1} (- z) \in ℝ) \to (F^{-1} (- z) \in [- 1, 1] \leftrightarrow - F^{-1} (- z) \in [- 1, - -1])$
102	11 12 101	mp3an12	$⊢ F^{-1} (- z) \in ℝ \to (F^{-1} (- z) \in [- 1, 1] \leftrightarrow - F^{-1} (- z) \in [- 1, - -1])$
103	100 102	syl	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to (F^{-1} (- z) \in [- 1, 1] \leftrightarrow - F^{-1} (- z) \in [- 1, - -1])$
104	97 103	mpbid	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to - F^{-1} (- z) \in [- 1, - -1]$
105		negneg1e1	$⊢ - -1 = 1$
106	105	oveq2i	$⊢ [- 1, - -1] = [- 1, 1]$
107	104 106	eleqtrdi	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to - F^{-1} (- z) \in [- 1, 1]$
108		xle0neg2	$⊢ z \in ℝ^{*} \to (0 \leq z \leftrightarrow - z \leq 0)$
109	108	notbid	$⊢ z \in ℝ^{*} \to (\neg 0 \leq z \leftrightarrow \neg - z \leq 0)$
110	109	biimpa	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to \neg - z \leq 0$
111		f1ocnvfv2	$⊢ (F : [0, 1] \underset{1-1 onto}{⟶} [0, +∞] \land - z \in [0, +∞]) \to F (F^{-1} (- z)) = - z$
112	22 94 111	sylancr	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to F (F^{-1} (- z)) = - z$
113		0elunit	$⊢ 0 \in [0, 1]$
114		ax-1ne0	$⊢ 1 \neq 0$
115		neeq2	$⊢ x = 0 \to (1 \neq x \leftrightarrow 1 \neq 0)$
116	114 115	mpbiri	$⊢ x = 0 \to 1 \neq x$
117	116	necomd	$⊢ x = 0 \to x \neq 1$
118		ifnefalse	$⊢ x \neq 1 \to if (x = 1, +∞, \frac{x}{1 - x}) = \frac{x}{1 - x}$
119	117 118	syl	$⊢ x = 0 \to if (x = 1, +∞, \frac{x}{1 - x}) = \frac{x}{1 - x}$
120		id	$⊢ x = 0 \to x = 0$
121		oveq2	$⊢ x = 0 \to 1 - x = 1 - 0$
122		1m0e1	$⊢ 1 - 0 = 1$
123	121 122	eqtrdi	$⊢ x = 0 \to 1 - x = 1$
124	120 123	oveq12d	$⊢ x = 0 \to \frac{x}{1 - x} = \frac{0}{1}$
125		ax-1cn	$⊢ 1 \in ℂ$
126	125 114	div0i	$⊢ \frac{0}{1} = 0$
127	124 126	eqtrdi	$⊢ x = 0 \to \frac{x}{1 - x} = 0$
128	119 127	eqtrd	$⊢ x = 0 \to if (x = 1, +∞, \frac{x}{1 - x}) = 0$
129		c0ex	$⊢ 0 \in V$
130	128 1 129	fvmpt	$⊢ 0 \in [0, 1] \to F (0) = 0$
131	113 130	ax-mp	$⊢ F (0) = 0$
132	131	a1i	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to F (0) = 0$
133	112 132	breq12d	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to (F (F^{-1} (- z)) \leq F (0) \leftrightarrow - z \leq 0)$
134	110 133	mtbird	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to \neg F (F^{-1} (- z)) \leq F (0)$
135		eqid	$⊢ ordTop (\leq) ↾_{𝑡} [0, +∞] = ordTop (\leq) ↾_{𝑡} [0, +∞]$
136	1 135	iccpnfhmeo	$⊢ (F {Isom}_{<, <} ([0, 1], [0, +∞]) \land F \in (II Homeo (ordTop (\leq) ↾_{𝑡} [0, +∞])))$
137	136	simpli	$⊢ F {Isom}_{<, <} ([0, 1], [0, +∞])$
138		iccssxr	$⊢ [0, 1] \subseteq ℝ^{*}$
139	138 10	pm3.2i	$⊢ ([0, 1] \subseteq ℝ^{} \land [0, +∞] \subseteq ℝ^{})$
140		leisorel	$⊢ (F {Isom}_{<, <} ([0, 1], [0, +∞]) \land ([0, 1] \subseteq ℝ^{} \land [0, +∞] \subseteq ℝ^{}) \land (F^{-1} (- z) \in [0, 1] \land 0 \in [0, 1])) \to (F^{-1} (- z) \leq 0 \leftrightarrow F (F^{-1} (- z)) \leq F (0))$
141	137 139 140	mp3an12	$⊢ (F^{-1} (- z) \in [0, 1] \land 0 \in [0, 1]) \to (F^{-1} (- z) \leq 0 \leftrightarrow F (F^{-1} (- z)) \leq F (0))$
142	96 113 141	sylancl	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to (F^{-1} (- z) \leq 0 \leftrightarrow F (F^{-1} (- z)) \leq F (0))$
143	134 142	mtbird	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to \neg F^{-1} (- z) \leq 0$
144	100	le0neg1d	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to (F^{-1} (- z) \leq 0 \leftrightarrow 0 \leq - F^{-1} (- z))$
145	143 144	mtbid	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to \neg 0 \leq - F^{-1} (- z)$
146		unitssre	$⊢ [0, 1] \subseteq ℝ$
147	146 96	sselid	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to F^{-1} (- z) \in ℝ$
148	147	recnd	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to F^{-1} (- z) \in ℂ$
149	148	negnegd	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to - (- F^{-1} (- z)) = F^{-1} (- z)$
150	149	fveq2d	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to F (- (- F^{-1} (- z))) = F (F^{-1} (- z))$
151	150 112	eqtrd	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to F (- (- F^{-1} (- z))) = - z$
152		xnegeq	$⊢ F (- (- F^{-1} (- z))) = - z \to - F (- (- F^{-1} (- z))) = - (- z)$
153	151 152	syl	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to - F (- (- F^{-1} (- z))) = - (- z)$
154		xnegneg	$⊢ z \in ℝ^{*} \to - (- z) = z$
155	154	adantr	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to - (- z) = z$
156	153 155	eqtr2d	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to z = - F (- (- F^{-1} (- z)))$
157		breq2	$⊢ y = - F^{-1} (- z) \to (0 \leq y \leftrightarrow 0 \leq - F^{-1} (- z))$
158	157	notbid	$⊢ y = - F^{-1} (- z) \to (\neg 0 \leq y \leftrightarrow \neg 0 \leq - F^{-1} (- z))$
159		negeq	$⊢ y = - F^{-1} (- z) \to - y = - (- F^{-1} (- z))$
160	159	fveq2d	$⊢ y = - F^{-1} (- z) \to F (- y) = F (- (- F^{-1} (- z)))$
161		xnegeq	$⊢ F (- y) = F (- (- F^{-1} (- z))) \to - F (- y) = - F (- (- F^{-1} (- z)))$
162	160 161	syl	$⊢ y = - F^{-1} (- z) \to - F (- y) = - F (- (- F^{-1} (- z)))$
163	162	eqeq2d	$⊢ y = - F^{-1} (- z) \to (z = - F (- y) \leftrightarrow z = - F (- (- F^{-1} (- z))))$
164	158 163	anbi12d	$⊢ y = - F^{-1} (- z) \to ((\neg 0 \leq y \land z = - F (- y)) \leftrightarrow (\neg 0 \leq - F^{-1} (- z) \land z = - F (- (- F^{-1} (- z)))))$
165	164	rspcev	$⊢ (- F^{-1} (- z) \in [- 1, 1] \land (\neg 0 \leq - F^{-1} (- z) \land z = - F (- (- F^{-1} (- z))))) \to \exists y \in [- 1, 1] (\neg 0 \leq y \land z = - F (- y))$
166	107 145 156 165	syl12anc	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to \exists y \in [- 1, 1] (\neg 0 \leq y \land z = - F (- y))$
167		iffalse	$⊢ \neg 0 \leq y \to if (0 \leq y, F (y), - F (- y)) = - F (- y)$
168	167	eqeq2d	$⊢ \neg 0 \leq y \to (z = if (0 \leq y, F (y), - F (- y)) \leftrightarrow z = - F (- y))$
169	168	biimpar	$⊢ (\neg 0 \leq y \land z = - F (- y)) \to z = if (0 \leq y, F (y), - F (- y))$
170	169	reximi	$⊢ \exists y \in [- 1, 1] (\neg 0 \leq y \land z = - F (- y)) \to \exists y \in [- 1, 1] z = if (0 \leq y, F (y), - F (- y))$
171	166 170	syl	$⊢ (z \in ℝ^{*} \land \neg 0 \leq z) \to \exists y \in [- 1, 1] z = if (0 \leq y, F (y), - F (- y))$
172	83 171	pm2.61dan	$⊢ z \in ℝ^{*} \to \exists y \in [- 1, 1] z = if (0 \leq y, F (y), - F (- y))$
173	51 172	mprgbir	$⊢ ℝ^{*} \subseteq \{z \| \exists y \in [- 1, 1] z = if (0 \leq y, F (y), - F (- y))\}$
174	2	rnmpt	$⊢ ran G = \{z \| \exists y \in [- 1, 1] z = if (0 \leq y, F (y), - F (- y))\}$
175	173 174	sseqtrri	$⊢ ℝ^{*} \subseteq ran G$
176	50 175	eqssi	$⊢ ran G = ℝ^{*}$
177		dffo2	$⊢ G : [- 1, 1] \underset{onto}{⟶} ℝ^{} \leftrightarrow (G : [- 1, 1] ⟶ ℝ^{} \land ran G = ℝ^{*})$
178	48 176 177	mpbir2an	$⊢ G : [- 1, 1] \underset{onto}{⟶} ℝ^{*}$
179		breq1	$⊢ F (z) = if (0 \leq z, F (z), - F (- z)) \to (F (z) < if (0 \leq w, F (w), - F (- w)) \leftrightarrow if (0 \leq z, F (z), - F (- z)) < if (0 \leq w, F (w), - F (- w)))$
180		breq1	$⊢ - F (- z) = if (0 \leq z, F (z), - F (- z)) \to (- F (- z) < if (0 \leq w, F (w), - F (- w)) \leftrightarrow if (0 \leq z, F (z), - F (- z)) < if (0 \leq w, F (w), - F (- w)))$
181		simpl3	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to z < w$
182		simpl1	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to z \in [- 1, 1]$
183		simpr	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to 0 \leq z$
184		breq2	$⊢ y = z \to (0 \leq y \leftrightarrow 0 \leq z)$
185		eleq1w	$⊢ y = z \to (y \in [0, 1] \leftrightarrow z \in [0, 1])$
186	184 185	imbi12d	$⊢ y = z \to ((0 \leq y \to y \in [0, 1]) \leftrightarrow (0 \leq z \to z \in [0, 1]))$
187	20	ex	$⊢ y \in [- 1, 1] \to (0 \leq y \to y \in [0, 1])$
188	186 187	vtoclga	$⊢ z \in [- 1, 1] \to (0 \leq z \to z \in [0, 1])$
189	182 183 188	sylc	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to z \in [0, 1]$
190		simpl2	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to w \in [- 1, 1]$
191	30	a1i	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to 0 \in ℝ$
192	99 182	sselid	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to z \in ℝ$
193	99 190	sselid	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to w \in ℝ$
194	192 193 181	ltled	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to z \leq w$
195	191 192 193 183 194	letrd	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to 0 \leq w$
196		breq2	$⊢ y = w \to (0 \leq y \leftrightarrow 0 \leq w)$
197		eleq1w	$⊢ y = w \to (y \in [0, 1] \leftrightarrow w \in [0, 1])$
198	196 197	imbi12d	$⊢ y = w \to ((0 \leq y \to y \in [0, 1]) \leftrightarrow (0 \leq w \to w \in [0, 1]))$
199	198 187	vtoclga	$⊢ w \in [- 1, 1] \to (0 \leq w \to w \in [0, 1])$
200	190 195 199	sylc	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to w \in [0, 1]$
201		isorel	$⊢ (F {Isom}_{<, <} ([0, 1], [0, +∞]) \land (z \in [0, 1] \land w \in [0, 1])) \to (z < w \leftrightarrow F (z) < F (w))$
202	137 201	mpan	$⊢ (z \in [0, 1] \land w \in [0, 1]) \to (z < w \leftrightarrow F (z) < F (w))$
203	189 200 202	syl2anc	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to (z < w \leftrightarrow F (z) < F (w))$
204	181 203	mpbid	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to F (z) < F (w)$
205	195	iftrued	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to if (0 \leq w, F (w), - F (- w)) = F (w)$
206	204 205	breqtrrd	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land 0 \leq z) \to F (z) < if (0 \leq w, F (w), - F (- w))$
207		breq2	$⊢ F (w) = if (0 \leq w, F (w), - F (- w)) \to (- F (- z) < F (w) \leftrightarrow - F (- z) < if (0 \leq w, F (w), - F (- w)))$
208		breq2	$⊢ - F (- w) = if (0 \leq w, F (w), - F (- w)) \to (- F (- z) < - F (- w) \leftrightarrow - F (- z) < if (0 \leq w, F (w), - F (- w)))$
209		simpl1	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \to z \in [- 1, 1]$
210		simpr	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \to \neg 0 \leq z$
211	184	notbid	$⊢ y = z \to (\neg 0 \leq y \leftrightarrow \neg 0 \leq z)$
212		negeq	$⊢ y = z \to - y = - z$
213	212	eleq1d	$⊢ y = z \to (- y \in [0, 1] \leftrightarrow - z \in [0, 1])$
214	211 213	imbi12d	$⊢ y = z \to ((\neg 0 \leq y \to - y \in [0, 1]) \leftrightarrow (\neg 0 \leq z \to - z \in [0, 1]))$
215	42	ex	$⊢ y \in [- 1, 1] \to (\neg 0 \leq y \to - y \in [0, 1])$
216	214 215	vtoclga	$⊢ z \in [- 1, 1] \to (\neg 0 \leq z \to - z \in [0, 1])$
217	209 210 216	sylc	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \to - z \in [0, 1]$
218	217	adantr	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to - z \in [0, 1]$
219	24	ffvelrni	$⊢ - z \in [0, 1] \to F (- z) \in [0, +∞]$
220	218 219	syl	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to F (- z) \in [0, +∞]$
221	10 220	sselid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to F (- z) \in ℝ^{*}$
222	221	xnegcld	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to - F (- z) \in ℝ^{*}$
223	86	a1i	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to 0 \in ℝ^{*}$
224		simpll2	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to w \in [- 1, 1]$
225		simpr	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to 0 \leq w$
226	224 225 199	sylc	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to w \in [0, 1]$
227	24	ffvelrni	$⊢ w \in [0, 1] \to F (w) \in [0, +∞]$
228	226 227	syl	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to F (w) \in [0, +∞]$
229	10 228	sselid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to F (w) \in ℝ^{*}$
230	210	adantr	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to \neg 0 \leq z$
231		simpll1	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to z \in [- 1, 1]$
232	99 231	sselid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to z \in ℝ$
233		ltnle	$⊢ (z \in ℝ \land 0 \in ℝ) \to (z < 0 \leftrightarrow \neg 0 \leq z)$
234	232 30 233	sylancl	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to (z < 0 \leftrightarrow \neg 0 \leq z)$
235	230 234	mpbird	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to z < 0$
236	232	lt0neg1d	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to (z < 0 \leftrightarrow 0 < - z)$
237	235 236	mpbid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to 0 < - z$
238		isorel	$⊢ (F {Isom}_{<, <} ([0, 1], [0, +∞]) \land (0 \in [0, 1] \land - z \in [0, 1])) \to (0 < - z \leftrightarrow F (0) < F (- z))$
239	137 238	mpan	$⊢ (0 \in [0, 1] \land - z \in [0, 1]) \to (0 < - z \leftrightarrow F (0) < F (- z))$
240	113 218 239	sylancr	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to (0 < - z \leftrightarrow F (0) < F (- z))$
241	237 240	mpbid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to F (0) < F (- z)$
242	131 241	eqbrtrrid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to 0 < F (- z)$
243		xlt0neg2	$⊢ F (- z) \in ℝ^{*} \to (0 < F (- z) \leftrightarrow - F (- z) < 0)$
244	221 243	syl	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to (0 < F (- z) \leftrightarrow - F (- z) < 0)$
245	242 244	mpbid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to - F (- z) < 0$
246		elxrge0	$⊢ F (w) \in [0, +∞] \leftrightarrow (F (w) \in ℝ^{*} \land 0 \leq F (w))$
247	246	simprbi	$⊢ F (w) \in [0, +∞] \to 0 \leq F (w)$
248	228 247	syl	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to 0 \leq F (w)$
249	222 223 229 245 248	xrltletrd	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land 0 \leq w) \to - F (- z) < F (w)$
250		simpll3	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to z < w$
251		simpll1	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to z \in [- 1, 1]$
252	99 251	sselid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to z \in ℝ$
253		simpll2	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to w \in [- 1, 1]$
254	99 253	sselid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to w \in ℝ$
255	252 254	ltnegd	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to (z < w \leftrightarrow - w < - z)$
256	250 255	mpbid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to - w < - z$
257		simpr	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to \neg 0 \leq w$
258	196	notbid	$⊢ y = w \to (\neg 0 \leq y \leftrightarrow \neg 0 \leq w)$
259		negeq	$⊢ y = w \to - y = - w$
260	259	eleq1d	$⊢ y = w \to (- y \in [0, 1] \leftrightarrow - w \in [0, 1])$
261	258 260	imbi12d	$⊢ y = w \to ((\neg 0 \leq y \to - y \in [0, 1]) \leftrightarrow (\neg 0 \leq w \to - w \in [0, 1]))$
262	261 215	vtoclga	$⊢ w \in [- 1, 1] \to (\neg 0 \leq w \to - w \in [0, 1])$
263	253 257 262	sylc	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to - w \in [0, 1]$
264	217	adantr	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to - z \in [0, 1]$
265		isorel	$⊢ (F {Isom}_{<, <} ([0, 1], [0, +∞]) \land (- w \in [0, 1] \land - z \in [0, 1])) \to (- w < - z \leftrightarrow F (- w) < F (- z))$
266	137 265	mpan	$⊢ (- w \in [0, 1] \land - z \in [0, 1]) \to (- w < - z \leftrightarrow F (- w) < F (- z))$
267	263 264 266	syl2anc	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to (- w < - z \leftrightarrow F (- w) < F (- z))$
268	256 267	mpbid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to F (- w) < F (- z)$
269	24	ffvelrni	$⊢ - w \in [0, 1] \to F (- w) \in [0, +∞]$
270	263 269	syl	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to F (- w) \in [0, +∞]$
271	10 270	sselid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to F (- w) \in ℝ^{*}$
272	264 219	syl	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to F (- z) \in [0, +∞]$
273	10 272	sselid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to F (- z) \in ℝ^{*}$
274		xltneg	$⊢ (F (- w) \in ℝ^{} \land F (- z) \in ℝ^{}) \to (F (- w) < F (- z) \leftrightarrow - F (- z) < - F (- w))$
275	271 273 274	syl2anc	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to (F (- w) < F (- z) \leftrightarrow - F (- z) < - F (- w))$
276	268 275	mpbid	$⊢ (((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \land \neg 0 \leq w) \to - F (- z) < - F (- w)$
277	207 208 249 276	ifbothda	$⊢ ((z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \land \neg 0 \leq z) \to - F (- z) < if (0 \leq w, F (w), - F (- w))$
278	179 180 206 277	ifbothda	$⊢ (z \in [- 1, 1] \land w \in [- 1, 1] \land z < w) \to if (0 \leq z, F (z), - F (- z)) < if (0 \leq w, F (w), - F (- w))$
279	278	3expia	$⊢ (z \in [- 1, 1] \land w \in [- 1, 1]) \to (z < w \to if (0 \leq z, F (z), - F (- z)) < if (0 \leq w, F (w), - F (- w)))$
280		fveq2	$⊢ y = z \to F (y) = F (z)$
281	212	fveq2d	$⊢ y = z \to F (- y) = F (- z)$
282		xnegeq	$⊢ F (- y) = F (- z) \to - F (- y) = - F (- z)$
283	281 282	syl	$⊢ y = z \to - F (- y) = - F (- z)$
284	184 280 283	ifbieq12d	$⊢ y = z \to if (0 \leq y, F (y), - F (- y)) = if (0 \leq z, F (z), - F (- z))$
285		fvex	$⊢ F (z) \in V$
286		xnegex	$⊢ - F (- z) \in V$
287	285 286	ifex	$⊢ if (0 \leq z, F (z), - F (- z)) \in V$
288	284 2 287	fvmpt	$⊢ z \in [- 1, 1] \to G (z) = if (0 \leq z, F (z), - F (- z))$
289		fveq2	$⊢ y = w \to F (y) = F (w)$
290	259	fveq2d	$⊢ y = w \to F (- y) = F (- w)$
291		xnegeq	$⊢ F (- y) = F (- w) \to - F (- y) = - F (- w)$
292	290 291	syl	$⊢ y = w \to - F (- y) = - F (- w)$
293	196 289 292	ifbieq12d	$⊢ y = w \to if (0 \leq y, F (y), - F (- y)) = if (0 \leq w, F (w), - F (- w))$
294		fvex	$⊢ F (w) \in V$
295		xnegex	$⊢ - F (- w) \in V$
296	294 295	ifex	$⊢ if (0 \leq w, F (w), - F (- w)) \in V$
297	293 2 296	fvmpt	$⊢ w \in [- 1, 1] \to G (w) = if (0 \leq w, F (w), - F (- w))$
298	288 297	breqan12d	$⊢ (z \in [- 1, 1] \land w \in [- 1, 1]) \to (G (z) < G (w) \leftrightarrow if (0 \leq z, F (z), - F (- z)) < if (0 \leq w, F (w), - F (- w)))$
299	279 298	sylibrd	$⊢ (z \in [- 1, 1] \land w \in [- 1, 1]) \to (z < w \to G (z) < G (w))$
300	299	rgen2	$⊢ \forall z \in [- 1, 1] \forall w \in [- 1, 1] (z < w \to G (z) < G (w))$
301		soisoi	$⊢ ((< Or [- 1, 1] \land < Po ℝ^{}) \land (G : [- 1, 1] \underset{onto}{⟶} ℝ^{} \land \forall z \in [- 1, 1] \forall w \in [- 1, 1] (z < w \to G (z) < G (w)))) \to G {Isom}_{<, <} ([- 1, 1], ℝ^{*})$
302	7 9 178 300 301	mp4an	$⊢ G {Isom}_{<, <} ([- 1, 1], ℝ^{*})$
303		letsr	$⊢ \leq \in TosetRel$
304	303	elexi	$⊢ \leq \in V$
305	304	inex1	$⊢ \leq \cap ([- 1, 1] \times [- 1, 1]) \in V$
306		ssid	$⊢ ℝ^{} \subseteq ℝ^{}$
307		leiso	$⊢ ([- 1, 1] \subseteq ℝ^{} \land ℝ^{} \subseteq ℝ^{}) \to (G {Isom}_{<, <} ([- 1, 1], ℝ^{}) \leftrightarrow G {Isom}_{\leq, \leq} ([- 1, 1], ℝ^{*}))$
308	4 306 307	mp2an	$⊢ G {Isom}_{<, <} ([- 1, 1], ℝ^{}) \leftrightarrow G {Isom}_{\leq, \leq} ([- 1, 1], ℝ^{})$
309	302 308	mpbi	$⊢ G {Isom}_{\leq, \leq} ([- 1, 1], ℝ^{*})$
310		isores1	$⊢ G {Isom}_{\leq, \leq} ([- 1, 1], ℝ^{}) \leftrightarrow G {Isom}_{\leq \cap ([- 1, 1] \times [- 1, 1]), \leq} ([- 1, 1], ℝ^{})$
311	309 310	mpbi	$⊢ G {Isom}_{\leq \cap ([- 1, 1] \times [- 1, 1]), \leq} ([- 1, 1], ℝ^{*})$
312		tsrps	$⊢ \leq \in TosetRel \to \leq \in PosetRel$
313	303 312	ax-mp	$⊢ \leq \in PosetRel$
314		ledm	$⊢ ℝ^{*} = dom \leq$
315	314	psssdm	$⊢ (\leq \in PosetRel \land [- 1, 1] \subseteq ℝ^{*}) \to dom (\leq \cap ([- 1, 1] \times [- 1, 1])) = [- 1, 1]$
316	313 4 315	mp2an	$⊢ dom (\leq \cap ([- 1, 1] \times [- 1, 1])) = [- 1, 1]$
317	316	eqcomi	$⊢ [- 1, 1] = dom (\leq \cap ([- 1, 1] \times [- 1, 1]))$
318	317 314	ordthmeo	$⊢ (\leq \cap ([- 1, 1] \times [- 1, 1]) \in V \land \leq \in TosetRel \land G {Isom}_{\leq \cap ([- 1, 1] \times [- 1, 1]), \leq} ([- 1, 1], ℝ^{*})) \to G \in (ordTop (\leq \cap ([- 1, 1] \times [- 1, 1])) Homeo ordTop (\leq))$
319	305 303 311 318	mp3an	$⊢ G \in (ordTop (\leq \cap ([- 1, 1] \times [- 1, 1])) Homeo ordTop (\leq))$
320		eqid	$⊢ ordTop (\leq) = ordTop (\leq)$
321	3 320	xrrest2	$⊢ [- 1, 1] \subseteq ℝ \to J ↾_{𝑡} [- 1, 1] = ordTop (\leq) ↾_{𝑡} [- 1, 1]$
322	99 321	ax-mp	$⊢ J ↾_{𝑡} [- 1, 1] = ordTop (\leq) ↾_{𝑡} [- 1, 1]$
323		ordtresticc	$⊢ ordTop (\leq) ↾_{𝑡} [- 1, 1] = ordTop (\leq \cap ([- 1, 1] \times [- 1, 1]))$
324	322 323	eqtri	$⊢ J ↾_{𝑡} [- 1, 1] = ordTop (\leq \cap ([- 1, 1] \times [- 1, 1]))$
325	324	oveq1i	$⊢ (J ↾_{𝑡} [- 1, 1]) Homeo ordTop (\leq) = ordTop (\leq \cap ([- 1, 1] \times [- 1, 1])) Homeo ordTop (\leq)$
326	319 325	eleqtrri	$⊢ G \in ((J ↾_{𝑡} [- 1, 1]) Homeo ordTop (\leq))$
327	302 326	pm3.2i	$⊢ (G {Isom}_{<, <} ([- 1, 1], ℝ^{*}) \land G \in ((J ↾_{𝑡} [- 1, 1]) Homeo ordTop (\leq)))$

Metamath Proof Explorer

Theorem xrhmeo

Proof