xrsmopn

Description: The metric on the extended reals generates a topology, but this does not match the order topology on RR* ; for example { +oo } is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypotheses	xrsxmet.1	$⊢ D = dist (ℝ_{𝑠}^{*})$
	xrsmopn.1	$⊢ J = MetOpen (D)$
Assertion	xrsmopn	$⊢ ordTop (\leq) \subseteq J$

Proof

Step	Hyp	Ref	Expression
1		xrsxmet.1	$⊢ D = dist (ℝ_{𝑠}^{*})$
2		xrsmopn.1	$⊢ J = MetOpen (D)$
3		elssuni	$⊢ x \in ordTop (\leq) \to x \subseteq ⋃ ordTop (\leq)$
4		letopuni	$⊢ ℝ^{*} = ⋃ ordTop (\leq)$
5	3 4	sseqtrrdi	$⊢ x \in ordTop (\leq) \to x \subseteq ℝ^{*}$
6		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
7	6	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
8		letop	$⊢ ordTop (\leq) \in Top$
9		reex	$⊢ ℝ \in V$
10		elrestr	$⊢ (ordTop (\leq) \in Top \land ℝ \in V \land x \in ordTop (\leq)) \to x \cap ℝ \in (ordTop (\leq) ↾_{𝑡} ℝ)$
11	8 9 10	mp3an12	$⊢ x \in ordTop (\leq) \to x \cap ℝ \in (ordTop (\leq) ↾_{𝑡} ℝ)$
12	11	ad2antrr	$⊢ ((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \to x \cap ℝ \in (ordTop (\leq) ↾_{𝑡} ℝ)$
13		elin	$⊢ y \in (x \cap ℝ) \leftrightarrow (y \in x \land y \in ℝ)$
14	13	biimpri	$⊢ (y \in x \land y \in ℝ) \to y \in (x \cap ℝ)$
15	14	adantll	$⊢ ((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \to y \in (x \cap ℝ)$
16		eqid	$⊢ ordTop (\leq) ↾_{𝑡} ℝ = ordTop (\leq) ↾_{𝑡} ℝ$
17	16	xrtgioo	$⊢ topGen (ran (.)) = ordTop (\leq) ↾_{𝑡} ℝ$
18		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
19	6 18	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
20	17 19	eqtr3i	$⊢ ordTop (\leq) ↾_{𝑡} ℝ = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
21	20	mopni2	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land x \cap ℝ \in (ordTop (\leq) ↾_{𝑡} ℝ) \land y \in (x \cap ℝ)) \to \exists r \in ℝ^{+} y ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq x \cap ℝ$
22	7 12 15 21	mp3an2i	$⊢ ((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \to \exists r \in ℝ^{+} y ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq x \cap ℝ$
23	1	xrsxmet	$⊢ D \in ∞Met (ℝ^{*})$
24		simplr	$⊢ (((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \land r \in ℝ^{+}) \to y \in ℝ$
25		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
26		sseqin2	$⊢ ℝ \subseteq ℝ^{} \leftrightarrow ℝ^{} \cap ℝ = ℝ$
27	25 26	mpbi	$⊢ ℝ^{*} \cap ℝ = ℝ$
28	24 27	eleqtrrdi	$⊢ (((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \land r \in ℝ^{+}) \to y \in (ℝ^{*} \cap ℝ)$
29		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
30	29	adantl	$⊢ (((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \land r \in ℝ^{+}) \to r \in ℝ^{*}$
31	1	xrsdsre	$⊢ {D ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
32	31	eqcomi	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {D ↾}_{ℝ^{2}}$
33	32	blres	$⊢ (D \in ∞Met (ℝ^{}) \land y \in (ℝ^{} \cap ℝ) \land r \in ℝ^{*}) \to y ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (y ball (D) r) \cap ℝ$
34	23 28 30 33	mp3an2i	$⊢ (((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \land r \in ℝ^{+}) \to y ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (y ball (D) r) \cap ℝ$
35	1	xrsblre	$⊢ (y \in ℝ \land r \in ℝ^{*}) \to y ball (D) r \subseteq ℝ$
36	29 35	sylan2	$⊢ (y \in ℝ \land r \in ℝ^{+}) \to y ball (D) r \subseteq ℝ$
37	36	adantll	$⊢ (((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \land r \in ℝ^{+}) \to y ball (D) r \subseteq ℝ$
38		df-ss	$⊢ y ball (D) r \subseteq ℝ \leftrightarrow (y ball (D) r) \cap ℝ = y ball (D) r$
39	37 38	sylib	$⊢ (((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \land r \in ℝ^{+}) \to (y ball (D) r) \cap ℝ = y ball (D) r$
40	34 39	eqtrd	$⊢ (((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \land r \in ℝ^{+}) \to y ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = y ball (D) r$
41	40	sseq1d	$⊢ (((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \land r \in ℝ^{+}) \to (y ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq x \cap ℝ \leftrightarrow y ball (D) r \subseteq x \cap ℝ)$
42		inss1	$⊢ x \cap ℝ \subseteq x$
43		sstr	$⊢ (y ball (D) r \subseteq x \cap ℝ \land x \cap ℝ \subseteq x) \to y ball (D) r \subseteq x$
44	42 43	mpan2	$⊢ y ball (D) r \subseteq x \cap ℝ \to y ball (D) r \subseteq x$
45	41 44	syl6bi	$⊢ (((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \land r \in ℝ^{+}) \to (y ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq x \cap ℝ \to y ball (D) r \subseteq x)$
46	45	reximdva	$⊢ ((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \to (\exists r \in ℝ^{+} y ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq x \cap ℝ \to \exists r \in ℝ^{+} y ball (D) r \subseteq x)$
47	22 46	mpd	$⊢ ((x \in ordTop (\leq) \land y \in x) \land y \in ℝ) \to \exists r \in ℝ^{+} y ball (D) r \subseteq x$
48		1rp	$⊢ 1 \in ℝ^{+}$
49	5	sselda	$⊢ (x \in ordTop (\leq) \land y \in x) \to y \in ℝ^{*}$
50	49	adantr	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ) \to y \in ℝ^{*}$
51		rpxr	$⊢ 1 \in ℝ^{+} \to 1 \in ℝ^{*}$
52	48 51	mp1i	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ) \to 1 \in ℝ^{*}$
53		elbl	$⊢ (D \in ∞Met (ℝ^{}) \land y \in ℝ^{} \land 1 \in ℝ^{}) \to (z \in (y ball (D) 1) \leftrightarrow (z \in ℝ^{} \land y D z < 1))$
54	23 50 52 53	mp3an2i	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ) \to (z \in (y ball (D) 1) \leftrightarrow (z \in ℝ^{*} \land y D z < 1))$
55		simp2	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \to \neg y \in ℝ$
56	49	3ad2ant1	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{} \land y D z < 1)) \to y \in ℝ^{}$
57	56	adantr	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{} \land y D z < 1)) \land y \neq z) \to y \in ℝ^{}$
58		simpl3l	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{} \land y D z < 1)) \land y \neq z) \to z \in ℝ^{}$
59		xmetcl	$⊢ (D \in ∞Met (ℝ^{}) \land y \in ℝ^{} \land z \in ℝ^{}) \to y D z \in ℝ^{}$
60	23 57 58 59	mp3an2i	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{} \land y D z < 1)) \land y \neq z) \to y D z \in ℝ^{}$
61		1red	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to 1 \in ℝ$
62		xmetge0	$⊢ (D \in ∞Met (ℝ^{}) \land y \in ℝ^{} \land z \in ℝ^{*}) \to 0 \leq y D z$
63	23 57 58 62	mp3an2i	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to 0 \leq y D z$
64		simpl3r	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to y D z < 1$
65		1xr	$⊢ 1 \in ℝ^{*}$
66		xrltle	$⊢ (y D z \in ℝ^{} \land 1 \in ℝ^{}) \to (y D z < 1 \to y D z \leq 1)$
67	60 65 66	sylancl	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to (y D z < 1 \to y D z \leq 1)$
68	64 67	mpd	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to y D z \leq 1$
69		xrrege0	$⊢ ((y D z \in ℝ^{*} \land 1 \in ℝ) \land (0 \leq y D z \land y D z \leq 1)) \to y D z \in ℝ$
70	60 61 63 68 69	syl22anc	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to y D z \in ℝ$
71		simpr	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to y \neq z$
72	1	xrsdsreclb	$⊢ (y \in ℝ^{} \land z \in ℝ^{} \land y \neq z) \to (y D z \in ℝ \leftrightarrow (y \in ℝ \land z \in ℝ))$
73	57 58 71 72	syl3anc	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to (y D z \in ℝ \leftrightarrow (y \in ℝ \land z \in ℝ))$
74	70 73	mpbid	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to (y \in ℝ \land z \in ℝ)$
75	74	simpld	$⊢ (((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \land y \neq z) \to y \in ℝ$
76	75	ex	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \to (y \neq z \to y \in ℝ)$
77	76	necon1bd	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \to (\neg y \in ℝ \to y = z)$
78		simp1r	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \to y \in x$
79		elequ1	$⊢ y = z \to (y \in x \leftrightarrow z \in x)$
80	78 79	syl5ibcom	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \to (y = z \to z \in x)$
81	77 80	syld	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \to (\neg y \in ℝ \to z \in x)$
82	55 81	mpd	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ \land (z \in ℝ^{*} \land y D z < 1)) \to z \in x$
83	82	3expia	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ) \to ((z \in ℝ^{*} \land y D z < 1) \to z \in x)$
84	54 83	sylbid	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ) \to (z \in (y ball (D) 1) \to z \in x)$
85	84	ssrdv	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ) \to y ball (D) 1 \subseteq x$
86		oveq2	$⊢ r = 1 \to y ball (D) r = y ball (D) 1$
87	86	sseq1d	$⊢ r = 1 \to (y ball (D) r \subseteq x \leftrightarrow y ball (D) 1 \subseteq x)$
88	87	rspcev	$⊢ (1 \in ℝ^{+} \land y ball (D) 1 \subseteq x) \to \exists r \in ℝ^{+} y ball (D) r \subseteq x$
89	48 85 88	sylancr	$⊢ ((x \in ordTop (\leq) \land y \in x) \land \neg y \in ℝ) \to \exists r \in ℝ^{+} y ball (D) r \subseteq x$
90	47 89	pm2.61dan	$⊢ (x \in ordTop (\leq) \land y \in x) \to \exists r \in ℝ^{+} y ball (D) r \subseteq x$
91	90	ralrimiva	$⊢ x \in ordTop (\leq) \to \forall y \in x \exists r \in ℝ^{+} y ball (D) r \subseteq x$
92	2	elmopn2	$⊢ D \in ∞Met (ℝ^{}) \to (x \in J \leftrightarrow (x \subseteq ℝ^{} \land \forall y \in x \exists r \in ℝ^{+} y ball (D) r \subseteq x))$
93	23 92	ax-mp	$⊢ x \in J \leftrightarrow (x \subseteq ℝ^{*} \land \forall y \in x \exists r \in ℝ^{+} y ball (D) r \subseteq x)$
94	5 91 93	sylanbrc	$⊢ x \in ordTop (\leq) \to x \in J$
95	94	ssriv	$⊢ ordTop (\leq) \subseteq J$

Metamath Proof Explorer

Theorem xrsmopn

Proof