relowlssretop

Description: The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020)

		Ref	Expression
	Hypothesis	relowlssretop.1	$⊢ I = [.) [ℝ^{2}]$
	Assertion	relowlssretop	$⊢ topGen (ran (.)) \subseteq topGen (I)$

Proof

Step	Hyp	Ref	Expression
1		relowlssretop.1	$⊢ I = [.) [ℝ^{2}]$
2		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
3		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
4		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (o \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} o = (a, b))$
5	2 3 4	mp2b	$⊢ o \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} o = (a, b)$
6		elxr	$⊢ b \in ℝ^{*} \leftrightarrow (b \in ℝ \lor b = +∞ \lor b = −∞)$
7		simpr	$⊢ (a \in ℝ^{*} \land b \in ℝ) \to b \in ℝ$
8		elioore	$⊢ x \in (a, b) \to x \in ℝ$
9	7 8	anim12ci	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to (x \in ℝ \land b \in ℝ)$
10	1	icoreelrn	$⊢ (x \in ℝ \land b \in ℝ) \to \{z \in ℝ \| (x \leq z \land z < b)\} \in I$
11	9 10	syl	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to \{z \in ℝ \| (x \leq z \land z < b)\} \in I$
12	8	adantl	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to x \in ℝ$
13	8	leidd	$⊢ x \in (a, b) \to x \leq x$
14	13	adantl	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to x \leq x$
15	7	rexrd	$⊢ (a \in ℝ^{} \land b \in ℝ) \to b \in ℝ^{}$
16		elioo1	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (x \in (a, b) \leftrightarrow (x \in ℝ^{*} \land a < x \land x < b))$
17	15 16	syldan	$⊢ (a \in ℝ^{} \land b \in ℝ) \to (x \in (a, b) \leftrightarrow (x \in ℝ^{} \land a < x \land x < b))$
18	17	biimpa	$⊢ ((a \in ℝ^{} \land b \in ℝ) \land x \in (a, b)) \to (x \in ℝ^{} \land a < x \land x < b)$
19	18	simp3d	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to x < b$
20		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
21	20	3anim1i	$⊢ (x \in ℝ \land x \leq x \land x < b) \to (x \in ℝ^{*} \land x \leq x \land x < b)$
22		rexr	$⊢ b \in ℝ \to b \in ℝ^{*}$
23		elico1	$⊢ (x \in ℝ^{} \land b \in ℝ^{}) \to (x \in [x, b) \leftrightarrow (x \in ℝ^{*} \land x \leq x \land x < b))$
24	20 22 23	syl2an	$⊢ (x \in ℝ \land b \in ℝ) \to (x \in [x, b) \leftrightarrow (x \in ℝ^{*} \land x \leq x \land x < b))$
25	24	biimprd	$⊢ (x \in ℝ \land b \in ℝ) \to ((x \in ℝ^{*} \land x \leq x \land x < b) \to x \in [x, b))$
26	9 21 25	syl2im	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to ((x \in ℝ \land x \leq x \land x < b) \to x \in [x, b))$
27		icoreval	$⊢ (x \in ℝ \land b \in ℝ) \to [x, b) = \{z \in ℝ \| (x \leq z \land z < b)\}$
28	9 27	syl	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to [x, b) = \{z \in ℝ \| (x \leq z \land z < b)\}$
29	28	eleq2d	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to (x \in [x, b) \leftrightarrow x \in \{z \in ℝ \| (x \leq z \land z < b)\})$
30	26 29	sylibd	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to ((x \in ℝ \land x \leq x \land x < b) \to x \in \{z \in ℝ \| (x \leq z \land z < b)\})$
31	12 14 19 30	mp3and	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to x \in \{z \in ℝ \| (x \leq z \land z < b)\}$
32		nfv	$⊢ Ⅎ z ((a \in ℝ^{} \land b \in ℝ^{}) \land x \in (a, b))$
33		nfrab1	$⊢ \underline{Ⅎ} z \{z \in ℝ \| (x \leq z \land z < b)\}$
34		nfcv	$⊢ \underline{Ⅎ} z (a, b)$
35		iooval	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (a, b) = \{x \in ℝ^{*} \| (a < x \land x < b)\}$
36	35	eleq2d	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (x \in (a, b) \leftrightarrow x \in \{x \in ℝ^{*} \| (a < x \land x < b)\})$
37	36	anbi1d	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to ((x \in (a, b) \land z \in \{z \in ℝ \| (x \leq z \land z < b)\}) \leftrightarrow (x \in \{x \in ℝ^{*} \| (a < x \land x < b)\} \land z \in \{z \in ℝ \| (x \leq z \land z < b)\}))$
38	37	pm5.32i	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land (x \in (a, b) \land z \in \{z \in ℝ \| (x \leq z \land z < b)\})) \leftrightarrow ((a \in ℝ^{} \land b \in ℝ^{}) \land (x \in \{x \in ℝ^{*} \| (a < x \land x < b)\} \land z \in \{z \in ℝ \| (x \leq z \land z < b)\}))$
39		rabid	$⊢ x \in \{x \in ℝ^{} \| (a < x \land x < b)\} \leftrightarrow (x \in ℝ^{} \land (a < x \land x < b))$
40		rabid	$⊢ z \in \{z \in ℝ \| (x \leq z \land z < b)\} \leftrightarrow (z \in ℝ \land (x \leq z \land z < b))$
41	39 40	anbi12i	$⊢ (x \in \{x \in ℝ^{} \| (a < x \land x < b)\} \land z \in \{z \in ℝ \| (x \leq z \land z < b)\}) \leftrightarrow ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))$
42		simpl	$⊢ (z \in ℝ \land (x \leq z \land z < b)) \to z \in ℝ$
43	42	rexrd	$⊢ (z \in ℝ \land (x \leq z \land z < b)) \to z \in ℝ^{*}$
44	43	ad2antll	$⊢ (a \in ℝ^{} \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to z \in ℝ^{*}$
45		simpl	$⊢ (x \in ℝ^{} \land (a < x \land x < b)) \to x \in ℝ^{}$
46	45 43	anim12i	$⊢ ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b))) \to (x \in ℝ^{} \land z \in ℝ^{*})$
47	46	anim2i	$⊢ (a \in ℝ^{} \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to (a \in ℝ^{} \land (x \in ℝ^{} \land z \in ℝ^{*}))$
48		3anass	$⊢ (a \in ℝ^{} \land x \in ℝ^{} \land z \in ℝ^{}) \leftrightarrow (a \in ℝ^{} \land (x \in ℝ^{} \land z \in ℝ^{}))$
49	47 48	sylibr	$⊢ (a \in ℝ^{} \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to (a \in ℝ^{} \land x \in ℝ^{} \land z \in ℝ^{*})$
50		simprl	$⊢ (x \in ℝ^{*} \land (a < x \land x < b)) \to a < x$
51		simprl	$⊢ (z \in ℝ \land (x \leq z \land z < b)) \to x \leq z$
52	50 51	anim12i	$⊢ ((x \in ℝ^{*} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b))) \to (a < x \land x \leq z)$
53	52	adantl	$⊢ (a \in ℝ^{} \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to (a < x \land x \leq z)$
54		xrltletr	$⊢ (a \in ℝ^{} \land x \in ℝ^{} \land z \in ℝ^{*}) \to ((a < x \land x \leq z) \to a < z)$
55	49 53 54	sylc	$⊢ (a \in ℝ^{} \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to a < z$
56		simprr	$⊢ (z \in ℝ \land (x \leq z \land z < b)) \to z < b$
57	56	ad2antll	$⊢ (a \in ℝ^{} \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to z < b$
58	55 57	jca	$⊢ (a \in ℝ^{} \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to (a < z \land z < b)$
59		rabid	$⊢ z \in \{z \in ℝ^{} \| (a < z \land z < b)\} \leftrightarrow (z \in ℝ^{} \land (a < z \land z < b))$
60	44 58 59	sylanbrc	$⊢ (a \in ℝ^{} \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to z \in \{z \in ℝ^{*} \| (a < z \land z < b)\}$
61	60	adantlr	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to z \in \{z \in ℝ^{} \| (a < z \land z < b)\}$
62		iooval	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (a, b) = \{z \in ℝ^{*} \| (a < z \land z < b)\}$
63	62	adantr	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land ((x \in ℝ^{} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to (a, b) = \{z \in ℝ^{} \| (a < z \land z < b)\}$
64	61 63	eleqtrrd	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land ((x \in ℝ^{*} \land (a < x \land x < b)) \land (z \in ℝ \land (x \leq z \land z < b)))) \to z \in (a, b)$
65	41 64	sylan2b	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land (x \in \{x \in ℝ^{*} \| (a < x \land x < b)\} \land z \in \{z \in ℝ \| (x \leq z \land z < b)\})) \to z \in (a, b)$
66	38 65	sylbi	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land (x \in (a, b) \land z \in \{z \in ℝ \| (x \leq z \land z < b)\})) \to z \in (a, b)$
67	66	expr	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land x \in (a, b)) \to (z \in \{z \in ℝ \| (x \leq z \land z < b)\} \to z \in (a, b))$
68	32 33 34 67	ssrd	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land x \in (a, b)) \to \{z \in ℝ \| (x \leq z \land z < b)\} \subseteq (a, b)$
69	22 68	sylanl2	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to \{z \in ℝ \| (x \leq z \land z < b)\} \subseteq (a, b)$
70		eleq2	$⊢ i = \{z \in ℝ \| (x \leq z \land z < b)\} \to (x \in i \leftrightarrow x \in \{z \in ℝ \| (x \leq z \land z < b)\})$
71		sseq1	$⊢ i = \{z \in ℝ \| (x \leq z \land z < b)\} \to (i \subseteq (a, b) \leftrightarrow \{z \in ℝ \| (x \leq z \land z < b)\} \subseteq (a, b))$
72	70 71	anbi12d	$⊢ i = \{z \in ℝ \| (x \leq z \land z < b)\} \to ((x \in i \land i \subseteq (a, b)) \leftrightarrow (x \in \{z \in ℝ \| (x \leq z \land z < b)\} \land \{z \in ℝ \| (x \leq z \land z < b)\} \subseteq (a, b)))$
73	72	rspcev	$⊢ (\{z \in ℝ \| (x \leq z \land z < b)\} \in I \land (x \in \{z \in ℝ \| (x \leq z \land z < b)\} \land \{z \in ℝ \| (x \leq z \land z < b)\} \subseteq (a, b))) \to \exists i \in I (x \in i \land i \subseteq (a, b))$
74	11 31 69 73	syl12anc	$⊢ ((a \in ℝ^{*} \land b \in ℝ) \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b))$
75	74	ancom1s	$⊢ ((b \in ℝ \land a \in ℝ^{*}) \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b))$
76	75	expl	$⊢ b \in ℝ \to ((a \in ℝ^{*} \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
77	8	adantl	$⊢ ((a \in ℝ^{*} \land b = +∞) \land x \in (a, b)) \to x \in ℝ$
78		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
79	1	icoreelrn	$⊢ (x \in ℝ \land x + 1 \in ℝ) \to \{z \in ℝ \| (x \leq z \land z < x + 1)\} \in I$
80	77 78 79	syl2anc2	$⊢ ((a \in ℝ^{*} \land b = +∞) \land x \in (a, b)) \to \{z \in ℝ \| (x \leq z \land z < x + 1)\} \in I$
81		elioore	$⊢ x \in (a, +∞) \to x \in ℝ$
82	81	adantl	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to x \in ℝ$
83	82	leidd	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to x \leq x$
84	82	ltp1d	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to x < x + 1$
85	82 83 84	jca32	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to (x \in ℝ \land (x \leq x \land x < x + 1))$
86		breq2	$⊢ z = x \to (x \leq z \leftrightarrow x \leq x)$
87		breq1	$⊢ z = x \to (z < x + 1 \leftrightarrow x < x + 1)$
88	86 87	anbi12d	$⊢ z = x \to ((x \leq z \land z < x + 1) \leftrightarrow (x \leq x \land x < x + 1))$
89	88	elrab	$⊢ x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \leftrightarrow (x \in ℝ \land (x \leq x \land x < x + 1))$
90	85 89	sylibr	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\}$
91		nfv	$⊢ Ⅎ z (a \in ℝ^{*} \land x \in (a, +∞))$
92		nfrab1	$⊢ \underline{Ⅎ} z \{z \in ℝ \| (x \leq z \land z < x + 1)\}$
93		nfcv	$⊢ \underline{Ⅎ} z (a, +∞)$
94		rabid	$⊢ z \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \leftrightarrow (z \in ℝ \land (x \leq z \land z < x + 1))$
95		simprl	$⊢ ((a \in ℝ^{*} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to z \in ℝ$
96		simpll	$⊢ ((a \in ℝ^{} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to a \in ℝ^{}$
97	82	adantr	$⊢ ((a \in ℝ^{*} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to x \in ℝ$
98	97	rexrd	$⊢ ((a \in ℝ^{} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to x \in ℝ^{}$
99	95	rexrd	$⊢ ((a \in ℝ^{} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to z \in ℝ^{}$
100		elioopnf	$⊢ a \in ℝ^{*} \to (x \in (a, +∞) \leftrightarrow (x \in ℝ \land a < x))$
101	100	simplbda	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to a < x$
102	101	adantr	$⊢ ((a \in ℝ^{*} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to a < x$
103		simprl	$⊢ (z \in ℝ \land (x \leq z \land z < x + 1)) \to x \leq z$
104	103	adantl	$⊢ ((a \in ℝ^{*} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to x \leq z$
105	96 98 99 102 104	xrltletrd	$⊢ ((a \in ℝ^{*} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to a < z$
106		elioopnf	$⊢ a \in ℝ^{*} \to (z \in (a, +∞) \leftrightarrow (z \in ℝ \land a < z))$
107	106	biimprd	$⊢ a \in ℝ^{*} \to ((z \in ℝ \land a < z) \to z \in (a, +∞))$
108	107	adantr	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to ((z \in ℝ \land a < z) \to z \in (a, +∞))$
109	108	adantr	$⊢ ((a \in ℝ^{*} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to ((z \in ℝ \land a < z) \to z \in (a, +∞))$
110	95 105 109	mp2and	$⊢ ((a \in ℝ^{*} \land x \in (a, +∞)) \land (z \in ℝ \land (x \leq z \land z < x + 1))) \to z \in (a, +∞)$
111	110	ex	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to ((z \in ℝ \land (x \leq z \land z < x + 1)) \to z \in (a, +∞))$
112	94 111	syl5bi	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to (z \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \to z \in (a, +∞))$
113	91 92 93 112	ssrd	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, +∞)$
114	90 113	jca	$⊢ (a \in ℝ^{*} \land x \in (a, +∞)) \to (x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, +∞))$
115		oveq2	$⊢ b = +∞ \to (a, b) = (a, +∞)$
116	115	eleq2d	$⊢ b = +∞ \to (x \in (a, b) \leftrightarrow x \in (a, +∞))$
117	116	anbi2d	$⊢ b = +∞ \to ((a \in ℝ^{} \land x \in (a, b)) \leftrightarrow (a \in ℝ^{} \land x \in (a, +∞)))$
118	115	sseq2d	$⊢ b = +∞ \to (\{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, b) \leftrightarrow \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, +∞))$
119	118	anbi2d	$⊢ b = +∞ \to ((x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, b)) \leftrightarrow (x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, +∞)))$
120	117 119	imbi12d	$⊢ b = +∞ \to (((a \in ℝ^{} \land x \in (a, b)) \to (x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, b))) \leftrightarrow ((a \in ℝ^{} \land x \in (a, +∞)) \to (x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, +∞))))$
121	114 120	mpbiri	$⊢ b = +∞ \to ((a \in ℝ^{*} \land x \in (a, b)) \to (x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, b)))$
122	121	impl	$⊢ ((b = +∞ \land a \in ℝ^{*}) \land x \in (a, b)) \to (x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, b))$
123	122	ancom1s	$⊢ ((a \in ℝ^{*} \land b = +∞) \land x \in (a, b)) \to (x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, b))$
124		eleq2	$⊢ i = \{z \in ℝ \| (x \leq z \land z < x + 1)\} \to (x \in i \leftrightarrow x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\})$
125		sseq1	$⊢ i = \{z \in ℝ \| (x \leq z \land z < x + 1)\} \to (i \subseteq (a, b) \leftrightarrow \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, b))$
126	124 125	anbi12d	$⊢ i = \{z \in ℝ \| (x \leq z \land z < x + 1)\} \to ((x \in i \land i \subseteq (a, b)) \leftrightarrow (x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, b)))$
127	126	rspcev	$⊢ (\{z \in ℝ \| (x \leq z \land z < x + 1)\} \in I \land (x \in \{z \in ℝ \| (x \leq z \land z < x + 1)\} \land \{z \in ℝ \| (x \leq z \land z < x + 1)\} \subseteq (a, b))) \to \exists i \in I (x \in i \land i \subseteq (a, b))$
128	80 123 127	syl2anc	$⊢ ((a \in ℝ^{*} \land b = +∞) \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b))$
129	128	ancom1s	$⊢ ((b = +∞ \land a \in ℝ^{*}) \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b))$
130	129	expl	$⊢ b = +∞ \to ((a \in ℝ^{*} \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
131	8	adantl	$⊢ ((a \in ℝ^{*} \land b = −∞) \land x \in (a, b)) \to x \in ℝ$
132		oveq2	$⊢ b = −∞ \to (a, b) = (a, −∞)$
133	132	eleq2d	$⊢ b = −∞ \to (x \in (a, b) \leftrightarrow x \in (a, −∞))$
134	133	adantl	$⊢ (a \in ℝ^{*} \land b = −∞) \to (x \in (a, b) \leftrightarrow x \in (a, −∞))$
135	134	pm5.32i	$⊢ ((a \in ℝ^{} \land b = −∞) \land x \in (a, b)) \leftrightarrow ((a \in ℝ^{} \land b = −∞) \land x \in (a, −∞))$
136		nltmnf	$⊢ x \in ℝ^{*} \to \neg x < −∞$
137	136	intnand	$⊢ x \in ℝ^{*} \to \neg (a < x \land x < −∞)$
138		eliooord	$⊢ x \in (a, −∞) \to (a < x \land x < −∞)$
139	137 138	nsyl	$⊢ x \in ℝ^{*} \to \neg x \in (a, −∞)$
140	139	pm2.21d	$⊢ x \in ℝ^{} \to (x \in (a, −∞) \to ((a \in ℝ^{} \land b = −∞) \to \exists i \in I (x \in i \land i \subseteq (a, b))))$
141	140	impd	$⊢ x \in ℝ^{} \to ((x \in (a, −∞) \land (a \in ℝ^{} \land b = −∞)) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
142	141	ancomsd	$⊢ x \in ℝ^{} \to (((a \in ℝ^{} \land b = −∞) \land x \in (a, −∞)) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
143	135 142	syl5bi	$⊢ x \in ℝ^{} \to (((a \in ℝ^{} \land b = −∞) \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
144	20 143	syl	$⊢ x \in ℝ \to (((a \in ℝ^{*} \land b = −∞) \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
145	131 144	mpcom	$⊢ ((a \in ℝ^{*} \land b = −∞) \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b))$
146	145	ancom1s	$⊢ ((b = −∞ \land a \in ℝ^{*}) \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b))$
147	146	expl	$⊢ b = −∞ \to ((a \in ℝ^{*} \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
148	76 130 147	3jaoi	$⊢ (b \in ℝ \lor b = +∞ \lor b = −∞) \to ((a \in ℝ^{*} \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
149	6 148	sylbi	$⊢ b \in ℝ^{} \to ((a \in ℝ^{} \land x \in (a, b)) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
150	149	expdimp	$⊢ (b \in ℝ^{} \land a \in ℝ^{}) \to (x \in (a, b) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
151	150	ancoms	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (x \in (a, b) \to \exists i \in I (x \in i \land i \subseteq (a, b)))$
152		eleq2	$⊢ o = (a, b) \to (x \in o \leftrightarrow x \in (a, b))$
153		sseq2	$⊢ o = (a, b) \to (i \subseteq o \leftrightarrow i \subseteq (a, b))$
154	153	anbi2d	$⊢ o = (a, b) \to ((x \in i \land i \subseteq o) \leftrightarrow (x \in i \land i \subseteq (a, b)))$
155	154	rexbidv	$⊢ o = (a, b) \to (\exists i \in I (x \in i \land i \subseteq o) \leftrightarrow \exists i \in I (x \in i \land i \subseteq (a, b)))$
156	152 155	imbi12d	$⊢ o = (a, b) \to ((x \in o \to \exists i \in I (x \in i \land i \subseteq o)) \leftrightarrow (x \in (a, b) \to \exists i \in I (x \in i \land i \subseteq (a, b))))$
157	151 156	syl5ibrcom	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (o = (a, b) \to (x \in o \to \exists i \in I (x \in i \land i \subseteq o)))$
158	157	rexlimivv	$⊢ \exists a \in ℝ^{} \exists b \in ℝ^{} o = (a, b) \to (x \in o \to \exists i \in I (x \in i \land i \subseteq o))$
159	5 158	sylbi	$⊢ o \in ran (.) \to (x \in o \to \exists i \in I (x \in i \land i \subseteq o))$
160	159	rgen	$⊢ \forall o \in ran (.) (x \in o \to \exists i \in I (x \in i \land i \subseteq o))$
161	160	rgenw	$⊢ \forall x \in ℝ \forall o \in ran (.) (x \in o \to \exists i \in I (x \in i \land i \subseteq o))$
162		iooex	$⊢ (.) \in V$
163	162	rnex	$⊢ ran (.) \in V$
164		unirnioo	$⊢ ℝ = ⋃ ran (.)$
165	1	icoreunrn	$⊢ ℝ = ⋃ I$
166	164 165	eqtr3i	$⊢ ⋃ ran (.) = ⋃ I$
167		tgss2	$⊢ (ran (.) \in V \land ⋃ ran (.) = ⋃ I) \to (topGen (ran (.)) \subseteq topGen (I) \leftrightarrow \forall x \in ⋃ ran (.) \forall o \in ran (.) (x \in o \to \exists i \in I (x \in i \land i \subseteq o)))$
168	163 166 167	mp2an	$⊢ topGen (ran (.)) \subseteq topGen (I) \leftrightarrow \forall x \in ⋃ ran (.) \forall o \in ran (.) (x \in o \to \exists i \in I (x \in i \land i \subseteq o))$
169	164	raleqi	$⊢ \forall x \in ℝ \forall o \in ran (.) (x \in o \to \exists i \in I (x \in i \land i \subseteq o)) \leftrightarrow \forall x \in ⋃ ran (.) \forall o \in ran (.) (x \in o \to \exists i \in I (x \in i \land i \subseteq o))$
170	168 169	bitr4i	$⊢ topGen (ran (.)) \subseteq topGen (I) \leftrightarrow \forall x \in ℝ \forall o \in ran (.) (x \in o \to \exists i \in I (x \in i \land i \subseteq o))$
171	161 170	mpbir	$⊢ topGen (ran (.)) \subseteq topGen (I)$

Metamath Proof Explorer

Theorem relowlssretop

Proof