Theorem 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	⊢ 𝐹 = ( 𝑥 ∈ ran [,] ↦ ( ℝ* ∖ 𝑥 ) )
Assertion	lecldbas	⊢ ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ran 𝐹 ) )

Proof

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