lecldbas

Description: The set of closed intervals forms a closed subbasis for the topology on the extended reals. Since our definition of a basis is in terms of open sets, we express this by showing that the complements of closed intervals form an open subbasis for the topology. (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Hypothesis	lecldbas.1	$⊢ F = (x \in ran [.] ⟼ ℝ^{*} ∖ x)$
	Assertion	lecldbas	$⊢ ordTop (\leq) = topGen (fi (ran F))$

Proof

Step	Hyp	Ref	Expression
1		lecldbas.1	$⊢ F = (x \in ran [.] ⟼ ℝ^{*} ∖ x)$
2		eqid	$⊢ ran (y \in ℝ^{} ⟼ (y, +∞]) = ran (y \in ℝ^{} ⟼ (y, +∞])$
3		eqid	$⊢ ran (y \in ℝ^{} ⟼ [−∞, y)) = ran (y \in ℝ^{} ⟼ [−∞, y))$
4	2 3	leordtval2	$⊢ ordTop (\leq) = topGen (fi (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))))$
5		fvex	$⊢ fi (ran F) \in V$
6		fvex	$⊢ ordTop (\leq) \in V$
7		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
8		ffn	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{} \to [.] Fn (ℝ^{} \times ℝ^{*})$
9	7 8	ax-mp	$⊢ [.] Fn (ℝ^{} \times ℝ^{})$
10		ovelrn	$⊢ [.] Fn (ℝ^{} \times ℝ^{}) \to (x \in ran [.] \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} x = [a, b])$
11	9 10	ax-mp	$⊢ x \in ran [.] \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} x = [a, b]$
12		difeq2	$⊢ x = [a, b] \to ℝ^{} ∖ x = ℝ^{} ∖ [a, b]$
13		iccordt	$⊢ [a, b] \in Clsd (ordTop (\leq))$
14		letopuni	$⊢ ℝ^{*} = ⋃ ordTop (\leq)$
15	14	cldopn	$⊢ [a, b] \in Clsd (ordTop (\leq)) \to ℝ^{*} ∖ [a, b] \in ordTop (\leq)$
16	13 15	ax-mp	$⊢ ℝ^{*} ∖ [a, b] \in ordTop (\leq)$
17	12 16	eqeltrdi	$⊢ x = [a, b] \to ℝ^{*} ∖ x \in ordTop (\leq)$
18	17	rexlimivw	$⊢ \exists b \in ℝ^{} x = [a, b] \to ℝ^{} ∖ x \in ordTop (\leq)$
19	18	rexlimivw	$⊢ \exists a \in ℝ^{} \exists b \in ℝ^{} x = [a, b] \to ℝ^{*} ∖ x \in ordTop (\leq)$
20	11 19	sylbi	$⊢ x \in ran [.] \to ℝ^{*} ∖ x \in ordTop (\leq)$
21	1 20	fmpti	$⊢ F : ran [.] ⟶ ordTop (\leq)$
22		frn	$⊢ F : ran [.] ⟶ ordTop (\leq) \to ran F \subseteq ordTop (\leq)$
23	21 22	ax-mp	$⊢ ran F \subseteq ordTop (\leq)$
24	6 23	ssexi	$⊢ ran F \in V$
25		eqid	$⊢ (y \in ℝ^{} ⟼ (y, +∞]) = (y \in ℝ^{} ⟼ (y, +∞])$
26		mnfxr	$⊢ −∞ \in ℝ^{*}$
27		fnovrn	$⊢ ([.] Fn (ℝ^{} \times ℝ^{}) \land −∞ \in ℝ^{} \land y \in ℝ^{}) \to [−∞, y] \in ran [.]$
28	9 26 27	mp3an12	$⊢ y \in ℝ^{*} \to [−∞, y] \in ran [.]$
29	26	a1i	$⊢ y \in ℝ^{} \to −∞ \in ℝ^{}$
30		id	$⊢ y \in ℝ^{} \to y \in ℝ^{}$
31		pnfxr	$⊢ +∞ \in ℝ^{*}$
32	31	a1i	$⊢ y \in ℝ^{} \to +∞ \in ℝ^{}$
33		mnfle	$⊢ y \in ℝ^{*} \to −∞ \leq y$
34		pnfge	$⊢ y \in ℝ^{*} \to y \leq +∞$
35		df-icc	$⊢ [.] = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{c \in ℝ^{*} \| (a \leq c \land c \leq b)\})$
36		df-ioc	$⊢ (.] = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{c \in ℝ^{*} \| (a < c \land c \leq b)\})$
37		xrltnle	$⊢ (y \in ℝ^{} \land z \in ℝ^{}) \to (y < z \leftrightarrow \neg z \leq y)$
38		xrletr	$⊢ (z \in ℝ^{} \land y \in ℝ^{} \land +∞ \in ℝ^{*}) \to ((z \leq y \land y \leq +∞) \to z \leq +∞)$
39		xrlelttr	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \to ((−∞ \leq y \land y < z) \to −∞ < z)$
40		xrltle	$⊢ (−∞ \in ℝ^{} \land z \in ℝ^{}) \to (−∞ < z \to −∞ \leq z)$
41	40	3adant2	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \to (−∞ < z \to −∞ \leq z)$
42	39 41	syld	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \to ((−∞ \leq y \land y < z) \to −∞ \leq z)$
43	35 36 37 35 38 42	ixxun	$⊢ ((−∞ \in ℝ^{} \land y \in ℝ^{} \land +∞ \in ℝ^{*}) \land (−∞ \leq y \land y \leq +∞)) \to [−∞, y] \cup (y, +∞] = [−∞, +∞]$
44	29 30 32 33 34 43	syl32anc	$⊢ y \in ℝ^{*} \to [−∞, y] \cup (y, +∞] = [−∞, +∞]$
45		iccmax	$⊢ [−∞, +∞] = ℝ^{*}$
46	44 45	eqtrdi	$⊢ y \in ℝ^{} \to [−∞, y] \cup (y, +∞] = ℝ^{}$
47		iccssxr	$⊢ [−∞, y] \subseteq ℝ^{*}$
48	35 36 37	ixxdisj	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{} \land +∞ \in ℝ^{*}) \to [−∞, y] \cap (y, +∞] = \emptyset$
49	26 31 48	mp3an13	$⊢ y \in ℝ^{*} \to [−∞, y] \cap (y, +∞] = \emptyset$
50		uneqdifeq	$⊢ ([−∞, y] \subseteq ℝ^{} \land [−∞, y] \cap (y, +∞] = \emptyset) \to ([−∞, y] \cup (y, +∞] = ℝ^{} \leftrightarrow ℝ^{*} ∖ [−∞, y] = (y, +∞])$
51	47 49 50	sylancr	$⊢ y \in ℝ^{} \to ([−∞, y] \cup (y, +∞] = ℝ^{} \leftrightarrow ℝ^{*} ∖ [−∞, y] = (y, +∞])$
52	46 51	mpbid	$⊢ y \in ℝ^{} \to ℝ^{} ∖ [−∞, y] = (y, +∞]$
53	52	eqcomd	$⊢ y \in ℝ^{} \to (y, +∞] = ℝ^{} ∖ [−∞, y]$
54		difeq2	$⊢ x = [−∞, y] \to ℝ^{} ∖ x = ℝ^{} ∖ [−∞, y]$
55	54	rspceeqv	$⊢ ([−∞, y] \in ran [.] \land (y, +∞] = ℝ^{} ∖ [−∞, y]) \to \exists x \in ran [.] (y, +∞] = ℝ^{} ∖ x$
56	28 53 55	syl2anc	$⊢ y \in ℝ^{} \to \exists x \in ran [.] (y, +∞] = ℝ^{} ∖ x$
57		xrex	$⊢ ℝ^{*} \in V$
58	57	difexi	$⊢ ℝ^{*} ∖ x \in V$
59	1 58	elrnmpti	$⊢ (y, +∞] \in ran F \leftrightarrow \exists x \in ran [.] (y, +∞] = ℝ^{*} ∖ x$
60	56 59	sylibr	$⊢ y \in ℝ^{*} \to (y, +∞] \in ran F$
61	25 60	fmpti	$⊢ (y \in ℝ^{} ⟼ (y, +∞]) : ℝ^{} ⟶ ran F$
62		frn	$⊢ (y \in ℝ^{} ⟼ (y, +∞]) : ℝ^{} ⟶ ran F \to ran (y \in ℝ^{*} ⟼ (y, +∞]) \subseteq ran F$
63	61 62	ax-mp	$⊢ ran (y \in ℝ^{*} ⟼ (y, +∞]) \subseteq ran F$
64		eqid	$⊢ (y \in ℝ^{} ⟼ [−∞, y)) = (y \in ℝ^{} ⟼ [−∞, y))$
65		fnovrn	$⊢ ([.] Fn (ℝ^{} \times ℝ^{}) \land y \in ℝ^{} \land +∞ \in ℝ^{}) \to [y, +∞] \in ran [.]$
66	9 31 65	mp3an13	$⊢ y \in ℝ^{*} \to [y, +∞] \in ran [.]$
67		df-ico	$⊢ [.) = (a \in ℝ^{}, b \in ℝ^{} ⟼ \{c \in ℝ^{*} \| (a \leq c \land c < b)\})$
68		xrlenlt	$⊢ (y \in ℝ^{} \land z \in ℝ^{}) \to (y \leq z \leftrightarrow \neg z < y)$
69		xrltletr	$⊢ (z \in ℝ^{} \land y \in ℝ^{} \land +∞ \in ℝ^{*}) \to ((z < y \land y \leq +∞) \to z < +∞)$
70		xrltle	$⊢ (z \in ℝ^{} \land +∞ \in ℝ^{}) \to (z < +∞ \to z \leq +∞)$
71	70	3adant2	$⊢ (z \in ℝ^{} \land y \in ℝ^{} \land +∞ \in ℝ^{*}) \to (z < +∞ \to z \leq +∞)$
72	69 71	syld	$⊢ (z \in ℝ^{} \land y \in ℝ^{} \land +∞ \in ℝ^{*}) \to ((z < y \land y \leq +∞) \to z \leq +∞)$
73		xrletr	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \to ((−∞ \leq y \land y \leq z) \to −∞ \leq z)$
74	67 35 68 35 72 73	ixxun	$⊢ ((−∞ \in ℝ^{} \land y \in ℝ^{} \land +∞ \in ℝ^{*}) \land (−∞ \leq y \land y \leq +∞)) \to [−∞, y) \cup [y, +∞] = [−∞, +∞]$
75	29 30 32 33 34 74	syl32anc	$⊢ y \in ℝ^{*} \to [−∞, y) \cup [y, +∞] = [−∞, +∞]$
76		uncom	$⊢ [−∞, y) \cup [y, +∞] = [y, +∞] \cup [−∞, y)$
77	75 76 45	3eqtr3g	$⊢ y \in ℝ^{} \to [y, +∞] \cup [−∞, y) = ℝ^{}$
78		iccssxr	$⊢ [y, +∞] \subseteq ℝ^{*}$
79		incom	$⊢ [y, +∞] \cap [−∞, y) = [−∞, y) \cap [y, +∞]$
80	67 35 68	ixxdisj	$⊢ (−∞ \in ℝ^{} \land y \in ℝ^{} \land +∞ \in ℝ^{*}) \to [−∞, y) \cap [y, +∞] = \emptyset$
81	26 31 80	mp3an13	$⊢ y \in ℝ^{*} \to [−∞, y) \cap [y, +∞] = \emptyset$
82	79 81	syl5eq	$⊢ y \in ℝ^{*} \to [y, +∞] \cap [−∞, y) = \emptyset$
83		uneqdifeq	$⊢ ([y, +∞] \subseteq ℝ^{} \land [y, +∞] \cap [−∞, y) = \emptyset) \to ([y, +∞] \cup [−∞, y) = ℝ^{} \leftrightarrow ℝ^{*} ∖ [y, +∞] = [−∞, y))$
84	78 82 83	sylancr	$⊢ y \in ℝ^{} \to ([y, +∞] \cup [−∞, y) = ℝ^{} \leftrightarrow ℝ^{*} ∖ [y, +∞] = [−∞, y))$
85	77 84	mpbid	$⊢ y \in ℝ^{} \to ℝ^{} ∖ [y, +∞] = [−∞, y)$
86	85	eqcomd	$⊢ y \in ℝ^{} \to [−∞, y) = ℝ^{} ∖ [y, +∞]$
87		difeq2	$⊢ x = [y, +∞] \to ℝ^{} ∖ x = ℝ^{} ∖ [y, +∞]$
88	87	rspceeqv	$⊢ ([y, +∞] \in ran [.] \land [−∞, y) = ℝ^{} ∖ [y, +∞]) \to \exists x \in ran [.] [−∞, y) = ℝ^{} ∖ x$
89	66 86 88	syl2anc	$⊢ y \in ℝ^{} \to \exists x \in ran [.] [−∞, y) = ℝ^{} ∖ x$
90	1 58	elrnmpti	$⊢ [−∞, y) \in ran F \leftrightarrow \exists x \in ran [.] [−∞, y) = ℝ^{*} ∖ x$
91	89 90	sylibr	$⊢ y \in ℝ^{*} \to [−∞, y) \in ran F$
92	64 91	fmpti	$⊢ (y \in ℝ^{} ⟼ [−∞, y)) : ℝ^{} ⟶ ran F$
93		frn	$⊢ (y \in ℝ^{} ⟼ [−∞, y)) : ℝ^{} ⟶ ran F \to ran (y \in ℝ^{*} ⟼ [−∞, y)) \subseteq ran F$
94	92 93	ax-mp	$⊢ ran (y \in ℝ^{*} ⟼ [−∞, y)) \subseteq ran F$
95	63 94	unssi	$⊢ ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y)) \subseteq ran F$
96		fiss	$⊢ (ran F \in V \land ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y)) \subseteq ran F) \to fi (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \subseteq fi (ran F)$
97	24 95 96	mp2an	$⊢ fi (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \subseteq fi (ran F)$
98		tgss	$⊢ (fi (ran F) \in V \land fi (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y))) \subseteq fi (ran F)) \to topGen (fi (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y)))) \subseteq topGen (fi (ran F))$
99	5 97 98	mp2an	$⊢ topGen (fi (ran (y \in ℝ^{} ⟼ (y, +∞]) \cup ran (y \in ℝ^{} ⟼ [−∞, y)))) \subseteq topGen (fi (ran F))$
100	4 99	eqsstri	$⊢ ordTop (\leq) \subseteq topGen (fi (ran F))$
101		letop	$⊢ ordTop (\leq) \in Top$
102		tgfiss	$⊢ (ordTop (\leq) \in Top \land ran F \subseteq ordTop (\leq)) \to topGen (fi (ran F)) \subseteq ordTop (\leq)$
103	101 23 102	mp2an	$⊢ topGen (fi (ran F)) \subseteq ordTop (\leq)$
104	100 103	eqssi	$⊢ ordTop (\leq) = topGen (fi (ran F))$

Metamath Proof Explorer

Theorem lecldbas

Proof