cnvordtrestixx

Description: The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017)

	Ref	Expression
Hypotheses	cnvordtrestixx.1	$⊢ A \subseteq ℝ^{*}$
	cnvordtrestixx.2	$⊢ (x \in A \land y \in A) \to [x, y] \subseteq A$
Assertion	cnvordtrestixx	$⊢ ordTop (\leq) ↾_{𝑡} A = ordTop (\leq^{-1} \cap (A \times A))$

Proof

Step	Hyp	Ref	Expression
1		cnvordtrestixx.1	$⊢ A \subseteq ℝ^{*}$
2		cnvordtrestixx.2	$⊢ (x \in A \land y \in A) \to [x, y] \subseteq A$
3		lern	$⊢ ℝ^{*} = ran \leq$
4		df-rn	$⊢ ran \leq = dom \leq^{-1}$
5	3 4	eqtri	$⊢ ℝ^{*} = dom \leq^{-1}$
6		letsr	$⊢ \leq \in TosetRel$
7		cnvtsr	$⊢ \leq \in TosetRel \to \leq^{-1} \in TosetRel$
8	6 7	ax-mp	$⊢ \leq^{-1} \in TosetRel$
9	8	a1i	$⊢ ⊤ \to \leq^{-1} \in TosetRel$
10	1	a1i	$⊢ ⊤ \to A \subseteq ℝ^{*}$
11		brcnvg	$⊢ (y \in A \land z \in ℝ^{*}) \to (y \leq^{-1} z \leftrightarrow z \leq y)$
12	11	adantlr	$⊢ ((y \in A \land x \in A) \land z \in ℝ^{*}) \to (y \leq^{-1} z \leftrightarrow z \leq y)$
13		simpr	$⊢ ((y \in A \land x \in A) \land z \in ℝ^{}) \to z \in ℝ^{}$
14		simplr	$⊢ ((y \in A \land x \in A) \land z \in ℝ^{*}) \to x \in A$
15		brcnvg	$⊢ (z \in ℝ^{*} \land x \in A) \to (z \leq^{-1} x \leftrightarrow x \leq z)$
16	13 14 15	syl2anc	$⊢ ((y \in A \land x \in A) \land z \in ℝ^{*}) \to (z \leq^{-1} x \leftrightarrow x \leq z)$
17	12 16	anbi12d	$⊢ ((y \in A \land x \in A) \land z \in ℝ^{*}) \to ((y \leq^{-1} z \land z \leq^{-1} x) \leftrightarrow (z \leq y \land x \leq z))$
18		ancom	$⊢ (z \leq y \land x \leq z) \leftrightarrow (x \leq z \land z \leq y)$
19	17 18	bitrdi	$⊢ ((y \in A \land x \in A) \land z \in ℝ^{*}) \to ((y \leq^{-1} z \land z \leq^{-1} x) \leftrightarrow (x \leq z \land z \leq y))$
20	19	rabbidva	$⊢ (y \in A \land x \in A) \to \{z \in ℝ^{} \| (y \leq^{-1} z \land z \leq^{-1} x)\} = \{z \in ℝ^{} \| (x \leq z \land z \leq y)\}$
21		simpr	$⊢ (y \in A \land x \in A) \to x \in A$
22	1 21	sselid	$⊢ (y \in A \land x \in A) \to x \in ℝ^{*}$
23		simpl	$⊢ (y \in A \land x \in A) \to y \in A$
24	1 23	sselid	$⊢ (y \in A \land x \in A) \to y \in ℝ^{*}$
25		iccval	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to [x, y] = \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\}$
26	22 24 25	syl2anc	$⊢ (y \in A \land x \in A) \to [x, y] = \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\}$
27	2	ancoms	$⊢ (y \in A \land x \in A) \to [x, y] \subseteq A$
28	26 27	eqsstrrd	$⊢ (y \in A \land x \in A) \to \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\} \subseteq A$
29	20 28	eqsstrd	$⊢ (y \in A \land x \in A) \to \{z \in ℝ^{*} \| (y \leq^{-1} z \land z \leq^{-1} x)\} \subseteq A$
30	29	adantl	$⊢ (⊤ \land (y \in A \land x \in A)) \to \{z \in ℝ^{*} \| (y \leq^{-1} z \land z \leq^{-1} x)\} \subseteq A$
31	5 9 10 30	ordtrest2	$⊢ ⊤ \to ordTop (\leq^{-1} \cap (A \times A)) = ordTop (\leq^{-1}) ↾_{𝑡} A$
32	31	mptru	$⊢ ordTop (\leq^{-1} \cap (A \times A)) = ordTop (\leq^{-1}) ↾_{𝑡} A$
33		tsrps	$⊢ \leq \in TosetRel \to \leq \in PosetRel$
34	6 33	ax-mp	$⊢ \leq \in PosetRel$
35		ordtcnv	$⊢ \leq \in PosetRel \to ordTop (\leq^{-1}) = ordTop (\leq)$
36	34 35	ax-mp	$⊢ ordTop (\leq^{-1}) = ordTop (\leq)$
37	36	oveq1i	$⊢ ordTop (\leq^{-1}) ↾_{𝑡} A = ordTop (\leq) ↾_{𝑡} A$
38	32 37	eqtr2i	$⊢ ordTop (\leq) ↾_{𝑡} A = ordTop (\leq^{-1} \cap (A \times A))$

Metamath Proof Explorer

Theorem cnvordtrestixx

Proof