xrtgioo

Description: The topology on the extended reals coincides with the standard topology on the reals, when restricted to RR . (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Hypothesis	xrtgioo.1	$⊢ J = ordTop (\leq) ↾_{𝑡} ℝ$
	Assertion	xrtgioo	$⊢ topGen (ran (.)) = J$

Proof

Step	Hyp	Ref	Expression
1		xrtgioo.1	$⊢ J = ordTop (\leq) ↾_{𝑡} ℝ$
2		letop	$⊢ ordTop (\leq) \in Top$
3		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
4		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
5	3 4	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
6		iooordt	$⊢ (x, y) \in ordTop (\leq)$
7	6	rgen2w	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} (x, y) \in ordTop (\leq)$
8		ffnov	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ ordTop (\leq) \leftrightarrow ((.) Fn (ℝ^{} \times ℝ^{}) \land \forall x \in ℝ^{} \forall y \in ℝ^{} (x, y) \in ordTop (\leq))$
9	5 7 8	mpbir2an	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ ordTop (\leq)$
10		frn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ ordTop (\leq) \to ran (.) \subseteq ordTop (\leq)$
11	9 10	ax-mp	$⊢ ran (.) \subseteq ordTop (\leq)$
12		tgss	$⊢ (ordTop (\leq) \in Top \land ran (.) \subseteq ordTop (\leq)) \to topGen (ran (.)) \subseteq topGen (ordTop (\leq))$
13	2 11 12	mp2an	$⊢ topGen (ran (.)) \subseteq topGen (ordTop (\leq))$
14		tgtop	$⊢ ordTop (\leq) \in Top \to topGen (ordTop (\leq)) = ordTop (\leq)$
15	2 14	ax-mp	$⊢ topGen (ordTop (\leq)) = ordTop (\leq)$
16	13 15	sseqtri	$⊢ topGen (ran (.)) \subseteq ordTop (\leq)$
17	16	sseli	$⊢ x \in topGen (ran (.)) \to x \in ordTop (\leq)$
18		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
19		toponss	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land x \in topGen (ran (.))) \to x \subseteq ℝ$
20	18 19	mpan	$⊢ x \in topGen (ran (.)) \to x \subseteq ℝ$
21		reordt	$⊢ ℝ \in ordTop (\leq)$
22		restopn2	$⊢ (ordTop (\leq) \in Top \land ℝ \in ordTop (\leq)) \to (x \in (ordTop (\leq) ↾_{𝑡} ℝ) \leftrightarrow (x \in ordTop (\leq) \land x \subseteq ℝ))$
23	2 21 22	mp2an	$⊢ x \in (ordTop (\leq) ↾_{𝑡} ℝ) \leftrightarrow (x \in ordTop (\leq) \land x \subseteq ℝ)$
24	17 20 23	sylanbrc	$⊢ x \in topGen (ran (.)) \to x \in (ordTop (\leq) ↾_{𝑡} ℝ)$
25	24	ssriv	$⊢ topGen (ran (.)) \subseteq ordTop (\leq) ↾_{𝑡} ℝ$
26		eqid	$⊢ ran (x \in ℝ^{} ⟼ (x, +∞]) = ran (x \in ℝ^{} ⟼ (x, +∞])$
27		eqid	$⊢ ran (x \in ℝ^{} ⟼ [−∞, x)) = ran (x \in ℝ^{} ⟼ [−∞, x))$
28		eqid	$⊢ ran (.) = ran (.)$
29	26 27 28	leordtval	$⊢ ordTop (\leq) = topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.))$
30	29	oveq1i	$⊢ ordTop (\leq) ↾_{𝑡} ℝ = topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ$
31	29 2	eqeltrri	$⊢ topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) \in Top$
32		tgclb	$⊢ (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \in TopBases \leftrightarrow topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) \in Top$
33	31 32	mpbir	$⊢ (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \in TopBases$
34		reex	$⊢ ℝ \in V$
35		tgrest	$⊢ ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \in TopBases \land ℝ \in V) \to topGen (((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ) = topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ$
36	33 34 35	mp2an	$⊢ topGen (((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ) = topGen ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ$
37	30 36	eqtr4i	$⊢ ordTop (\leq) ↾_{𝑡} ℝ = topGen (((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ)$
38		retopbas	$⊢ ran (.) \in TopBases$
39		elrest	$⊢ ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.) \in TopBases \land ℝ \in V) \to (u \in (((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ) \leftrightarrow \exists v \in ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) u = v \cap ℝ)$
40	33 34 39	mp2an	$⊢ u \in (((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ) \leftrightarrow \exists v \in ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) u = v \cap ℝ$
41		elun	$⊢ v \in ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) \leftrightarrow (v \in (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \lor v \in ran (.))$
42		elun	$⊢ v \in (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \leftrightarrow (v \in ran (x \in ℝ^{} ⟼ (x, +∞]) \lor v \in ran (x \in ℝ^{} ⟼ [−∞, x)))$
43		eqid	$⊢ (x \in ℝ^{} ⟼ (x, +∞]) = (x \in ℝ^{} ⟼ (x, +∞])$
44	43	elrnmpt	$⊢ v \in V \to (v \in ran (x \in ℝ^{} ⟼ (x, +∞]) \leftrightarrow \exists x \in ℝ^{} v = (x, +∞])$
45	44	elv	$⊢ v \in ran (x \in ℝ^{} ⟼ (x, +∞]) \leftrightarrow \exists x \in ℝ^{} v = (x, +∞]$
46		simpl	$⊢ (x \in ℝ^{} \land y \in ℝ) \to x \in ℝ^{}$
47		pnfxr	$⊢ +∞ \in ℝ^{*}$
48	47	a1i	$⊢ (x \in ℝ^{} \land y \in ℝ) \to +∞ \in ℝ^{}$
49		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
50	49	adantl	$⊢ (x \in ℝ^{} \land y \in ℝ) \to y \in ℝ^{}$
51		df-ioc	$⊢ (.] = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{c \in ℝ^{*} \| (a < c \land c \leq b)\})$
52	51	elixx3g	$⊢ y \in (x, +∞] \leftrightarrow ((x \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (x < y \land y \leq +∞))$
53	52	baib	$⊢ (x \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \to (y \in (x, +∞] \leftrightarrow (x < y \land y \leq +∞))$
54	46 48 50 53	syl3anc	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to (y \in (x, +∞] \leftrightarrow (x < y \land y \leq +∞))$
55		pnfge	$⊢ y \in ℝ^{*} \to y \leq +∞$
56	50 55	syl	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to y \leq +∞$
57	56	biantrud	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to (x < y \leftrightarrow (x < y \land y \leq +∞))$
58		ltpnf	$⊢ y \in ℝ \to y < +∞$
59	58	adantl	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to y < +∞$
60	59	biantrud	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to (x < y \leftrightarrow (x < y \land y < +∞))$
61	54 57 60	3bitr2d	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to (y \in (x, +∞] \leftrightarrow (x < y \land y < +∞))$
62	61	pm5.32da	$⊢ x \in ℝ^{*} \to ((y \in ℝ \land y \in (x, +∞]) \leftrightarrow (y \in ℝ \land (x < y \land y < +∞)))$
63		elin	$⊢ y \in ((x, +∞] \cap ℝ) \leftrightarrow (y \in (x, +∞] \land y \in ℝ)$
64	63	biancomi	$⊢ y \in ((x, +∞] \cap ℝ) \leftrightarrow (y \in ℝ \land y \in (x, +∞])$
65		3anass	$⊢ (y \in ℝ \land x < y \land y < +∞) \leftrightarrow (y \in ℝ \land (x < y \land y < +∞))$
66	62 64 65	3bitr4g	$⊢ x \in ℝ^{*} \to (y \in ((x, +∞] \cap ℝ) \leftrightarrow (y \in ℝ \land x < y \land y < +∞))$
67		elioo2	$⊢ (x \in ℝ^{} \land +∞ \in ℝ^{}) \to (y \in (x, +∞) \leftrightarrow (y \in ℝ \land x < y \land y < +∞))$
68	47 67	mpan2	$⊢ x \in ℝ^{*} \to (y \in (x, +∞) \leftrightarrow (y \in ℝ \land x < y \land y < +∞))$
69	66 68	bitr4d	$⊢ x \in ℝ^{*} \to (y \in ((x, +∞] \cap ℝ) \leftrightarrow y \in (x, +∞))$
70	69	eqrdv	$⊢ x \in ℝ^{*} \to (x, +∞] \cap ℝ = (x, +∞)$
71		ioorebas	$⊢ (x, +∞) \in ran (.)$
72	70 71	eqeltrdi	$⊢ x \in ℝ^{*} \to (x, +∞] \cap ℝ \in ran (.)$
73		ineq1	$⊢ v = (x, +∞] \to v \cap ℝ = (x, +∞] \cap ℝ$
74	73	eleq1d	$⊢ v = (x, +∞] \to (v \cap ℝ \in ran (.) \leftrightarrow (x, +∞] \cap ℝ \in ran (.))$
75	72 74	syl5ibrcom	$⊢ x \in ℝ^{*} \to (v = (x, +∞] \to v \cap ℝ \in ran (.))$
76	75	rexlimiv	$⊢ \exists x \in ℝ^{*} v = (x, +∞] \to v \cap ℝ \in ran (.)$
77	45 76	sylbi	$⊢ v \in ran (x \in ℝ^{*} ⟼ (x, +∞]) \to v \cap ℝ \in ran (.)$
78		eqid	$⊢ (x \in ℝ^{} ⟼ [−∞, x)) = (x \in ℝ^{} ⟼ [−∞, x))$
79	78	elrnmpt	$⊢ v \in V \to (v \in ran (x \in ℝ^{} ⟼ [−∞, x)) \leftrightarrow \exists x \in ℝ^{} v = [−∞, x))$
80	79	elv	$⊢ v \in ran (x \in ℝ^{} ⟼ [−∞, x)) \leftrightarrow \exists x \in ℝ^{} v = [−∞, x)$
81		mnfxr	$⊢ −∞ \in ℝ^{*}$
82	81	a1i	$⊢ (x \in ℝ^{} \land y \in ℝ) \to −∞ \in ℝ^{}$
83		df-ico	$⊢ [.) = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{c \in ℝ^{*} \| (a \leq c \land c < b)\})$
84	83	elixx3g	$⊢ y \in [−∞, x) \leftrightarrow ((−∞ \in ℝ^{} \land x \in ℝ^{} \land y \in ℝ^{*}) \land (−∞ \leq y \land y < x))$
85	84	baib	$⊢ (−∞ \in ℝ^{} \land x \in ℝ^{} \land y \in ℝ^{*}) \to (y \in [−∞, x) \leftrightarrow (−∞ \leq y \land y < x))$
86	82 46 50 85	syl3anc	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to (y \in [−∞, x) \leftrightarrow (−∞ \leq y \land y < x))$
87		mnfle	$⊢ y \in ℝ^{*} \to −∞ \leq y$
88	50 87	syl	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to −∞ \leq y$
89	88	biantrurd	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to (y < x \leftrightarrow (−∞ \leq y \land y < x))$
90		mnflt	$⊢ y \in ℝ \to −∞ < y$
91	90	adantl	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to −∞ < y$
92	91	biantrurd	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to (y < x \leftrightarrow (−∞ < y \land y < x))$
93	86 89 92	3bitr2d	$⊢ (x \in ℝ^{*} \land y \in ℝ) \to (y \in [−∞, x) \leftrightarrow (−∞ < y \land y < x))$
94	93	pm5.32da	$⊢ x \in ℝ^{*} \to ((y \in ℝ \land y \in [−∞, x)) \leftrightarrow (y \in ℝ \land (−∞ < y \land y < x)))$
95		elin	$⊢ y \in ([−∞, x) \cap ℝ) \leftrightarrow (y \in [−∞, x) \land y \in ℝ)$
96	95	biancomi	$⊢ y \in ([−∞, x) \cap ℝ) \leftrightarrow (y \in ℝ \land y \in [−∞, x))$
97		3anass	$⊢ (y \in ℝ \land −∞ < y \land y < x) \leftrightarrow (y \in ℝ \land (−∞ < y \land y < x))$
98	94 96 97	3bitr4g	$⊢ x \in ℝ^{*} \to (y \in ([−∞, x) \cap ℝ) \leftrightarrow (y \in ℝ \land −∞ < y \land y < x))$
99		elioo2	$⊢ (−∞ \in ℝ^{} \land x \in ℝ^{}) \to (y \in (−∞, x) \leftrightarrow (y \in ℝ \land −∞ < y \land y < x))$
100	81 99	mpan	$⊢ x \in ℝ^{*} \to (y \in (−∞, x) \leftrightarrow (y \in ℝ \land −∞ < y \land y < x))$
101	98 100	bitr4d	$⊢ x \in ℝ^{*} \to (y \in ([−∞, x) \cap ℝ) \leftrightarrow y \in (−∞, x))$
102	101	eqrdv	$⊢ x \in ℝ^{*} \to [−∞, x) \cap ℝ = (−∞, x)$
103		ioorebas	$⊢ (−∞, x) \in ran (.)$
104	102 103	eqeltrdi	$⊢ x \in ℝ^{*} \to [−∞, x) \cap ℝ \in ran (.)$
105		ineq1	$⊢ v = [−∞, x) \to v \cap ℝ = [−∞, x) \cap ℝ$
106	105	eleq1d	$⊢ v = [−∞, x) \to (v \cap ℝ \in ran (.) \leftrightarrow [−∞, x) \cap ℝ \in ran (.))$
107	104 106	syl5ibrcom	$⊢ x \in ℝ^{*} \to (v = [−∞, x) \to v \cap ℝ \in ran (.))$
108	107	rexlimiv	$⊢ \exists x \in ℝ^{*} v = [−∞, x) \to v \cap ℝ \in ran (.)$
109	80 108	sylbi	$⊢ v \in ran (x \in ℝ^{*} ⟼ [−∞, x)) \to v \cap ℝ \in ran (.)$
110	77 109	jaoi	$⊢ (v \in ran (x \in ℝ^{} ⟼ (x, +∞]) \lor v \in ran (x \in ℝ^{} ⟼ [−∞, x))) \to v \cap ℝ \in ran (.)$
111	42 110	sylbi	$⊢ v \in (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \to v \cap ℝ \in ran (.)$
112		elssuni	$⊢ v \in ran (.) \to v \subseteq ⋃ ran (.)$
113		unirnioo	$⊢ ℝ = ⋃ ran (.)$
114	112 113	sseqtrrdi	$⊢ v \in ran (.) \to v \subseteq ℝ$
115		dfss2	$⊢ v \subseteq ℝ \leftrightarrow v \cap ℝ = v$
116	114 115	sylib	$⊢ v \in ran (.) \to v \cap ℝ = v$
117		id	$⊢ v \in ran (.) \to v \in ran (.)$
118	116 117	eqeltrd	$⊢ v \in ran (.) \to v \cap ℝ \in ran (.)$
119	111 118	jaoi	$⊢ (v \in (ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \lor v \in ran (.)) \to v \cap ℝ \in ran (.)$
120	41 119	sylbi	$⊢ v \in ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) \to v \cap ℝ \in ran (.)$
121		eleq1	$⊢ u = v \cap ℝ \to (u \in ran (.) \leftrightarrow v \cap ℝ \in ran (.))$
122	120 121	syl5ibrcom	$⊢ v \in ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) \to (u = v \cap ℝ \to u \in ran (.))$
123	122	rexlimiv	$⊢ \exists v \in ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) u = v \cap ℝ \to u \in ran (.)$
124	40 123	sylbi	$⊢ u \in (((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ) \to u \in ran (.)$
125	124	ssriv	$⊢ ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ \subseteq ran (.)$
126		tgss	$⊢ (ran (.) \in TopBases \land ((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ \subseteq ran (.)) \to topGen (((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ) \subseteq topGen (ran (.))$
127	38 125 126	mp2an	$⊢ topGen (((ran (x \in ℝ^{} ⟼ (x, +∞]) \cup ran (x \in ℝ^{} ⟼ [−∞, x))) \cup ran (.)) ↾_{𝑡} ℝ) \subseteq topGen (ran (.))$
128	37 127	eqsstri	$⊢ ordTop (\leq) ↾_{𝑡} ℝ \subseteq topGen (ran (.))$
129	25 128	eqssi	$⊢ topGen (ran (.)) = ordTop (\leq) ↾_{𝑡} ℝ$
130	129 1	eqtr4i	$⊢ topGen (ran (.)) = J$

Metamath Proof Explorer

Theorem xrtgioo

Proof