relowlpssretop

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

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

Proof

Step	Hyp	Ref	Expression
1		relowlpssretop.1	$⊢ I = [.) [ℝ^{2}]$
2	1	relowlssretop	$⊢ topGen (ran (.)) \subseteq topGen (I)$
3		2re	$⊢ 2 \in ℝ$
4		1lt2	$⊢ 1 < 2$
5		ovex	$⊢ [1, c) \in V$
6		sbcan	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} (c \in ℝ \land x < c) \leftrightarrow (\underset{˙}{[} 1 / x \underset{˙}{]} c \in ℝ \land \underset{˙}{[} 1 / x \underset{˙}{]} x < c)$
7		1re	$⊢ 1 \in ℝ$
8		sbcg	$⊢ 1 \in ℝ \to (\underset{˙}{[} 1 / x \underset{˙}{]} c \in ℝ \leftrightarrow c \in ℝ)$
9	7 8	ax-mp	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} c \in ℝ \leftrightarrow c \in ℝ$
10		sbcbr123	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} x < c \leftrightarrow ⦋ 1 / x ⦌ x ⦋ 1 / x ⦌ < ⦋ 1 / x ⦌ c$
11		csbvarg	$⊢ 1 \in ℝ \to ⦋ 1 / x ⦌ x = 1$
12	7 11	ax-mp	$⊢ ⦋ 1 / x ⦌ x = 1$
13		csbconstg	$⊢ 1 \in ℝ \to ⦋ 1 / x ⦌ c = c$
14	7 13	ax-mp	$⊢ ⦋ 1 / x ⦌ c = c$
15	12 14	breq12i	$⊢ ⦋ 1 / x ⦌ x ⦋ 1 / x ⦌ < ⦋ 1 / x ⦌ c \leftrightarrow 1 ⦋ 1 / x ⦌ < c$
16		csbconstg	$⊢ 1 \in ℝ \to ⦋ 1 / x ⦌ < = <$
17	7 16	ax-mp	$⊢ ⦋ 1 / x ⦌ < = <$
18	17	breqi	$⊢ 1 ⦋ 1 / x ⦌ < c \leftrightarrow 1 < c$
19	10 15 18	3bitri	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} x < c \leftrightarrow 1 < c$
20	9 19	anbi12i	$⊢ (\underset{˙}{[} 1 / x \underset{˙}{]} c \in ℝ \land \underset{˙}{[} 1 / x \underset{˙}{]} x < c) \leftrightarrow (c \in ℝ \land 1 < c)$
21	6 20	bitri	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} (c \in ℝ \land x < c) \leftrightarrow (c \in ℝ \land 1 < c)$
22		sbceqg	$⊢ 1 \in ℝ \to (\underset{˙}{[} 1 / x \underset{˙}{]} i = [x, c) \leftrightarrow ⦋ 1 / x ⦌ i = ⦋ 1 / x ⦌ [x, c))$
23	7 22	ax-mp	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} i = [x, c) \leftrightarrow ⦋ 1 / x ⦌ i = ⦋ 1 / x ⦌ [x, c)$
24		csbconstg	$⊢ 1 \in ℝ \to ⦋ 1 / x ⦌ i = i$
25	7 24	ax-mp	$⊢ ⦋ 1 / x ⦌ i = i$
26		csbov123	$⊢ ⦋ 1 / x ⦌ [x, c) = ⦋ 1 / x ⦌ x ⦋ 1 / x ⦌ [.) ⦋ 1 / x ⦌ c$
27		csbconstg	$⊢ 1 \in ℝ \to ⦋ 1 / x ⦌ [.) = [.)$
28	7 27	ax-mp	$⊢ ⦋ 1 / x ⦌ [.) = [.)$
29	12 14 28	oveq123i	$⊢ ⦋ 1 / x ⦌ x ⦋ 1 / x ⦌ [.) ⦋ 1 / x ⦌ c = [1, c)$
30	26 29	eqtri	$⊢ ⦋ 1 / x ⦌ [x, c) = [1, c)$
31	25 30	eqeq12i	$⊢ ⦋ 1 / x ⦌ i = ⦋ 1 / x ⦌ [x, c) \leftrightarrow i = [1, c)$
32	23 31	bitri	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} i = [x, c) \leftrightarrow i = [1, c)$
33		sbcan	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} ((c \in ℝ \land x < c) \land i = [x, c)) \leftrightarrow (\underset{˙}{[} 1 / x \underset{˙}{]} (c \in ℝ \land x < c) \land \underset{˙}{[} 1 / x \underset{˙}{]} i = [x, c))$
34		simpr	$⊢ (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to x \in ℝ$
35		simpl	$⊢ (x \in ℝ \land c \in ℝ) \to x \in ℝ$
36		leid	$⊢ x \in ℝ \to x \leq x$
37	35 36	jccir	$⊢ (x \in ℝ \land c \in ℝ) \to (x \in ℝ \land x \leq x)$
38		rexr	$⊢ c \in ℝ \to c \in ℝ^{*}$
39		elico2	$⊢ (x \in ℝ \land c \in ℝ^{*}) \to (x \in [x, c) \leftrightarrow (x \in ℝ \land x \leq x \land x < c))$
40	38 39	sylan2	$⊢ (x \in ℝ \land c \in ℝ) \to (x \in [x, c) \leftrightarrow (x \in ℝ \land x \leq x \land x < c))$
41		df-3an	$⊢ (x \in ℝ \land x \leq x \land x < c) \leftrightarrow ((x \in ℝ \land x \leq x) \land x < c)$
42	40 41	bitrdi	$⊢ (x \in ℝ \land c \in ℝ) \to (x \in [x, c) \leftrightarrow ((x \in ℝ \land x \leq x) \land x < c))$
43	42	baibd	$⊢ ((x \in ℝ \land c \in ℝ) \land (x \in ℝ \land x \leq x)) \to (x \in [x, c) \leftrightarrow x < c)$
44	37 43	mpdan	$⊢ (x \in ℝ \land c \in ℝ) \to (x \in [x, c) \leftrightarrow x < c)$
45	44	biimpar	$⊢ ((x \in ℝ \land c \in ℝ) \land x < c) \to x \in [x, c)$
46	45	adantr	$⊢ (((x \in ℝ \land c \in ℝ) \land x < c) \land i = [x, c)) \to x \in [x, c)$
47		eleq2	$⊢ i = [x, c) \to (x \in i \leftrightarrow x \in [x, c))$
48	47	adantl	$⊢ (((x \in ℝ \land c \in ℝ) \land x < c) \land i = [x, c)) \to (x \in i \leftrightarrow x \in [x, c))$
49	46 48	mpbird	$⊢ (((x \in ℝ \land c \in ℝ) \land x < c) \land i = [x, c)) \to x \in i$
50		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
51		opelxpi	$⊢ (x \in ℝ \land c \in ℝ) \to ⟨x, c⟩ \in ℝ^{2}$
52	50 51	sselid	$⊢ (x \in ℝ \land c \in ℝ) \to ⟨x, c⟩ \in (ℝ^{} \times ℝ^{})$
53		df-ico	$⊢ [.) = (x \in ℝ^{}, c \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < c)\})$
54	53	ixxf	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
55	54	fdmi	$⊢ dom [.) = ℝ^{} \times ℝ^{}$
56	55	eleq2i	$⊢ ⟨x, c⟩ \in dom [.) \leftrightarrow ⟨x, c⟩ \in (ℝ^{} \times ℝ^{})$
57	53	mpofun	$⊢ Fun [.)$
58		funfvima	$⊢ (Fun [.) \land ⟨x, c⟩ \in dom [.)) \to (⟨x, c⟩ \in ℝ^{2} \to [.) (⟨x, c⟩) \in [.) [ℝ^{2}])$
59	57 58	mpan	$⊢ ⟨x, c⟩ \in dom [.) \to (⟨x, c⟩ \in ℝ^{2} \to [.) (⟨x, c⟩) \in [.) [ℝ^{2}])$
60	56 59	sylbir	$⊢ ⟨x, c⟩ \in (ℝ^{} \times ℝ^{}) \to (⟨x, c⟩ \in ℝ^{2} \to [.) (⟨x, c⟩) \in [.) [ℝ^{2}])$
61	52 51 60	sylc	$⊢ (x \in ℝ \land c \in ℝ) \to [.) (⟨x, c⟩) \in [.) [ℝ^{2}]$
62		df-ov	$⊢ [x, c) = [.) (⟨x, c⟩)$
63	61 62 1	3eltr4g	$⊢ (x \in ℝ \land c \in ℝ) \to [x, c) \in I$
64		eleq1	$⊢ i = [x, c) \to (i \in I \leftrightarrow [x, c) \in I)$
65	63 64	syl5ibrcom	$⊢ (x \in ℝ \land c \in ℝ) \to (i = [x, c) \to i \in I)$
66	65	imp	$⊢ ((x \in ℝ \land c \in ℝ) \land i = [x, c)) \to i \in I$
67		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
68		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
69	67 68	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
70		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (o \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} o = (a, b))$
71	69 70	ax-mp	$⊢ o \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} o = (a, b)$
72		iooelexlt	$⊢ x \in (a, b) \to \exists y \in (a, b) y < x$
73		df-rex	$⊢ \exists y \in (a, b) y < x \leftrightarrow \exists y (y \in (a, b) \land y < x)$
74	72 73	sylib	$⊢ x \in (a, b) \to \exists y (y \in (a, b) \land y < x)$
75		simpl	$⊢ (y \in (a, b) \land y < x) \to y \in (a, b)$
76	75	a1i	$⊢ x \in (a, b) \to ((y \in (a, b) \land y < x) \to y \in (a, b))$
77	53	elmpocl2	$⊢ y \in [x, c) \to c \in ℝ^{*}$
78		elioore	$⊢ x \in (a, b) \to x \in ℝ$
79		elico2	$⊢ (x \in ℝ \land c \in ℝ^{*}) \to (y \in [x, c) \leftrightarrow (y \in ℝ \land x \leq y \land y < c))$
80	78 79	sylan	$⊢ (x \in (a, b) \land c \in ℝ^{*}) \to (y \in [x, c) \leftrightarrow (y \in ℝ \land x \leq y \land y < c))$
81		simp2	$⊢ (y \in ℝ \land x \leq y \land y < c) \to x \leq y$
82	80 81	syl6bi	$⊢ (x \in (a, b) \land c \in ℝ^{*}) \to (y \in [x, c) \to x \leq y)$
83	82	ex	$⊢ x \in (a, b) \to (c \in ℝ^{*} \to (y \in [x, c) \to x \leq y))$
84	83	com23	$⊢ x \in (a, b) \to (y \in [x, c) \to (c \in ℝ^{*} \to x \leq y))$
85	77 84	mpdi	$⊢ x \in (a, b) \to (y \in [x, c) \to x \leq y)$
86	85	imp	$⊢ (x \in (a, b) \land y \in [x, c)) \to x \leq y$
87	78	rexrd	$⊢ x \in (a, b) \to x \in ℝ^{*}$
88	87	adantr	$⊢ (x \in (a, b) \land y \in [x, c)) \to x \in ℝ^{*}$
89		elicore	$⊢ (x \in ℝ \land y \in [x, c)) \to y \in ℝ$
90	78 89	sylan	$⊢ (x \in (a, b) \land y \in [x, c)) \to y \in ℝ$
91	90	rexrd	$⊢ (x \in (a, b) \land y \in [x, c)) \to y \in ℝ^{*}$
92		xrlenlt	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x \leq y \leftrightarrow \neg y < x)$
93	92	biimpd	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x \leq y \to \neg y < x)$
94	93	con2d	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (y < x \to \neg x \leq y)$
95	88 91 94	syl2anc	$⊢ (x \in (a, b) \land y \in [x, c)) \to (y < x \to \neg x \leq y)$
96	86 95	mt2d	$⊢ (x \in (a, b) \land y \in [x, c)) \to \neg y < x$
97	96	intnand	$⊢ (x \in (a, b) \land y \in [x, c)) \to \neg (y \in (a, b) \land y < x)$
98	97	ex	$⊢ x \in (a, b) \to (y \in [x, c) \to \neg (y \in (a, b) \land y < x))$
99	98	con2d	$⊢ x \in (a, b) \to ((y \in (a, b) \land y < x) \to \neg y \in [x, c))$
100	76 99	jcad	$⊢ x \in (a, b) \to ((y \in (a, b) \land y < x) \to (y \in (a, b) \land \neg y \in [x, c)))$
101		annim	$⊢ (y \in (a, b) \land \neg y \in [x, c)) \leftrightarrow \neg (y \in (a, b) \to y \in [x, c))$
102	100 101	syl6ib	$⊢ x \in (a, b) \to ((y \in (a, b) \land y < x) \to \neg (y \in (a, b) \to y \in [x, c)))$
103	102	eximdv	$⊢ x \in (a, b) \to (\exists y (y \in (a, b) \land y < x) \to \exists y \neg (y \in (a, b) \to y \in [x, c)))$
104	74 103	mpd	$⊢ x \in (a, b) \to \exists y \neg (y \in (a, b) \to y \in [x, c))$
105		exnal	$⊢ \exists y \neg (y \in (a, b) \to y \in [x, c)) \leftrightarrow \neg \forall y (y \in (a, b) \to y \in [x, c))$
106	104 105	sylib	$⊢ x \in (a, b) \to \neg \forall y (y \in (a, b) \to y \in [x, c))$
107		dfss2	$⊢ (a, b) \subseteq [x, c) \leftrightarrow \forall y (y \in (a, b) \to y \in [x, c))$
108	106 107	sylnibr	$⊢ x \in (a, b) \to \neg (a, b) \subseteq [x, c)$
109		imnan	$⊢ (x \in (a, b) \to \neg (a, b) \subseteq [x, c)) \leftrightarrow \neg (x \in (a, b) \land (a, b) \subseteq [x, c))$
110	108 109	mpbi	$⊢ \neg (x \in (a, b) \land (a, b) \subseteq [x, c))$
111		eleq2	$⊢ o = (a, b) \to (x \in o \leftrightarrow x \in (a, b))$
112		sseq1	$⊢ o = (a, b) \to (o \subseteq [x, c) \leftrightarrow (a, b) \subseteq [x, c))$
113	111 112	anbi12d	$⊢ o = (a, b) \to ((x \in o \land o \subseteq [x, c)) \leftrightarrow (x \in (a, b) \land (a, b) \subseteq [x, c)))$
114	110 113	mtbiri	$⊢ o = (a, b) \to \neg (x \in o \land o \subseteq [x, c))$
115		sseq2	$⊢ i = [x, c) \to (o \subseteq i \leftrightarrow o \subseteq [x, c))$
116	115	anbi2d	$⊢ i = [x, c) \to ((x \in o \land o \subseteq i) \leftrightarrow (x \in o \land o \subseteq [x, c)))$
117	116	notbid	$⊢ i = [x, c) \to (\neg (x \in o \land o \subseteq i) \leftrightarrow \neg (x \in o \land o \subseteq [x, c)))$
118	114 117	syl5ibrcom	$⊢ o = (a, b) \to (i = [x, c) \to \neg (x \in o \land o \subseteq i))$
119	118	a1i	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to (o = (a, b) \to (i = [x, c) \to \neg (x \in o \land o \subseteq i)))$
120	119	rexlimivv	$⊢ \exists a \in ℝ^{} \exists b \in ℝ^{} o = (a, b) \to (i = [x, c) \to \neg (x \in o \land o \subseteq i))$
121	71 120	sylbi	$⊢ o \in ran (.) \to (i = [x, c) \to \neg (x \in o \land o \subseteq i))$
122	121	com12	$⊢ i = [x, c) \to (o \in ran (.) \to \neg (x \in o \land o \subseteq i))$
123	122	ralrimiv	$⊢ i = [x, c) \to \forall o \in ran (.) \neg (x \in o \land o \subseteq i)$
124		ralnex	$⊢ \forall o \in ran (.) \neg (x \in o \land o \subseteq i) \leftrightarrow \neg \exists o \in ran (.) (x \in o \land o \subseteq i)$
125	123 124	sylib	$⊢ i = [x, c) \to \neg \exists o \in ran (.) (x \in o \land o \subseteq i)$
126	125	adantl	$⊢ ((x \in ℝ \land c \in ℝ) \land i = [x, c)) \to \neg \exists o \in ran (.) (x \in o \land o \subseteq i)$
127	66 126	jca	$⊢ ((x \in ℝ \land c \in ℝ) \land i = [x, c)) \to (i \in I \land \neg \exists o \in ran (.) (x \in o \land o \subseteq i))$
128	127	adantlr	$⊢ (((x \in ℝ \land c \in ℝ) \land x < c) \land i = [x, c)) \to (i \in I \land \neg \exists o \in ran (.) (x \in o \land o \subseteq i))$
129	49 128	jca	$⊢ (((x \in ℝ \land c \in ℝ) \land x < c) \land i = [x, c)) \to (x \in i \land (i \in I \land \neg \exists o \in ran (.) (x \in o \land o \subseteq i)))$
130		an12	$⊢ (x \in i \land (i \in I \land \neg \exists o \in ran (.) (x \in o \land o \subseteq i))) \leftrightarrow (i \in I \land (x \in i \land \neg \exists o \in ran (.) (x \in o \land o \subseteq i)))$
131		annim	$⊢ (x \in i \land \neg \exists o \in ran (.) (x \in o \land o \subseteq i)) \leftrightarrow \neg (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
132	131	anbi2i	$⊢ (i \in I \land (x \in i \land \neg \exists o \in ran (.) (x \in o \land o \subseteq i))) \leftrightarrow (i \in I \land \neg (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i)))$
133	130 132	bitri	$⊢ (x \in i \land (i \in I \land \neg \exists o \in ran (.) (x \in o \land o \subseteq i))) \leftrightarrow (i \in I \land \neg (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i)))$
134	129 133	sylib	$⊢ (((x \in ℝ \land c \in ℝ) \land x < c) \land i = [x, c)) \to (i \in I \land \neg (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i)))$
135		rspe	$⊢ (i \in I \land \neg (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))) \to \exists i \in I \neg (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
136	134 135	syl	$⊢ (((x \in ℝ \land c \in ℝ) \land x < c) \land i = [x, c)) \to \exists i \in I \neg (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
137		rexnal	$⊢ \exists i \in I \neg (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i)) \leftrightarrow \neg \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
138	136 137	sylib	$⊢ (((x \in ℝ \land c \in ℝ) \land x < c) \land i = [x, c)) \to \neg \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
139	138	exp41	$⊢ x \in ℝ \to (c \in ℝ \to (x < c \to (i = [x, c) \to \neg \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i)))))$
140	139	com4l	$⊢ c \in ℝ \to (x < c \to (i = [x, c) \to (x \in ℝ \to \neg \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i)))))$
141	140	imp41	$⊢ (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \neg \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
142		rspe	$⊢ (x \in ℝ \land \neg \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))) \to \exists x \in ℝ \neg \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
143	34 141 142	syl2anc	$⊢ (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \exists x \in ℝ \neg \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
144		rexnal	$⊢ \exists x \in ℝ \neg \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i)) \leftrightarrow \neg \forall x \in ℝ \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
145	143 144	sylib	$⊢ (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \neg \forall x \in ℝ \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
146		df-ico	$⊢ [.) = (m \in ℝ^{}, n \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (m \leq z \land z < n)\})$
147	146	ixxex	$⊢ [.) \in V$
148		imaexg	$⊢ [.) \in V \to [.) [ℝ^{2}] \in V$
149	147 148	ax-mp	$⊢ [.) [ℝ^{2}] \in V$
150	1 149	eqeltri	$⊢ I \in V$
151	1	icoreunrn	$⊢ ℝ = ⋃ I$
152		unirnioo	$⊢ ℝ = ⋃ ran (.)$
153	151 152	eqtr3i	$⊢ ⋃ I = ⋃ ran (.)$
154		tgss2	$⊢ (I \in V \land ⋃ I = ⋃ ran (.)) \to (topGen (I) \subseteq topGen (ran (.)) \leftrightarrow \forall x \in ⋃ I \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i)))$
155	150 153 154	mp2an	$⊢ topGen (I) \subseteq topGen (ran (.)) \leftrightarrow \forall x \in ⋃ I \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
156	151	raleqi	$⊢ \forall x \in ℝ \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i)) \leftrightarrow \forall x \in ⋃ I \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
157	155 156	bitr4i	$⊢ topGen (I) \subseteq topGen (ran (.)) \leftrightarrow \forall x \in ℝ \forall i \in I (x \in i \to \exists o \in ran (.) (x \in o \land o \subseteq i))$
158	145 157	sylnibr	$⊢ (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \neg topGen (I) \subseteq topGen (ran (.))$
159	158	sbcth	$⊢ 1 \in ℝ \to \underset{˙}{[} 1 / x \underset{˙}{]} ((((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \neg topGen (I) \subseteq topGen (ran (.)))$
160	7 159	ax-mp	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} ((((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \neg topGen (I) \subseteq topGen (ran (.)))$
161		sbcimg	$⊢ 1 \in ℝ \to (\underset{˙}{[} 1 / x \underset{˙}{]} ((((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \neg topGen (I) \subseteq topGen (ran (.))) \leftrightarrow (\underset{˙}{[} 1 / x \underset{˙}{]} (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \underset{˙}{[} 1 / x \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.))))$
162	7 161	ax-mp	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} ((((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \neg topGen (I) \subseteq topGen (ran (.))) \leftrightarrow (\underset{˙}{[} 1 / x \underset{˙}{]} (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \underset{˙}{[} 1 / x \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.)))$
163	160 162	mpbi	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \to \underset{˙}{[} 1 / x \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.))$
164		sbcel1v	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} x \in ℝ \leftrightarrow 1 \in ℝ$
165	7 164	mpbir	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} x \in ℝ$
166		sbcan	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \leftrightarrow (\underset{˙}{[} 1 / x \underset{˙}{]} ((c \in ℝ \land x < c) \land i = [x, c)) \land \underset{˙}{[} 1 / x \underset{˙}{]} x \in ℝ)$
167	165 166	mpbiran2	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} (((c \in ℝ \land x < c) \land i = [x, c)) \land x \in ℝ) \leftrightarrow \underset{˙}{[} 1 / x \underset{˙}{]} ((c \in ℝ \land x < c) \land i = [x, c))$
168		sbcg	$⊢ 1 \in ℝ \to (\underset{˙}{[} 1 / x \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.)) \leftrightarrow \neg topGen (I) \subseteq topGen (ran (.)))$
169	7 168	ax-mp	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.)) \leftrightarrow \neg topGen (I) \subseteq topGen (ran (.))$
170	163 167 169	3imtr3i	$⊢ \underset{˙}{[} 1 / x \underset{˙}{]} ((c \in ℝ \land x < c) \land i = [x, c)) \to \neg topGen (I) \subseteq topGen (ran (.))$
171	33 170	sylbir	$⊢ (\underset{˙}{[} 1 / x \underset{˙}{]} (c \in ℝ \land x < c) \land \underset{˙}{[} 1 / x \underset{˙}{]} i = [x, c)) \to \neg topGen (I) \subseteq topGen (ran (.))$
172	21 32 171	syl2anbr	$⊢ ((c \in ℝ \land 1 < c) \land i = [1, c)) \to \neg topGen (I) \subseteq topGen (ran (.))$
173	172	sbcth	$⊢ [1, c) \in V \to \underset{˙}{[} [1, c) / i \underset{˙}{]} (((c \in ℝ \land 1 < c) \land i = [1, c)) \to \neg topGen (I) \subseteq topGen (ran (.)))$
174	5 173	ax-mp	$⊢ \underset{˙}{[} [1, c) / i \underset{˙}{]} (((c \in ℝ \land 1 < c) \land i = [1, c)) \to \neg topGen (I) \subseteq topGen (ran (.)))$
175		sbcimg	$⊢ [1, c) \in V \to (\underset{˙}{[} [1, c) / i \underset{˙}{]} (((c \in ℝ \land 1 < c) \land i = [1, c)) \to \neg topGen (I) \subseteq topGen (ran (.))) \leftrightarrow (\underset{˙}{[} [1, c) / i \underset{˙}{]} ((c \in ℝ \land 1 < c) \land i = [1, c)) \to \underset{˙}{[} [1, c) / i \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.))))$
176	5 175	ax-mp	$⊢ \underset{˙}{[} [1, c) / i \underset{˙}{]} (((c \in ℝ \land 1 < c) \land i = [1, c)) \to \neg topGen (I) \subseteq topGen (ran (.))) \leftrightarrow (\underset{˙}{[} [1, c) / i \underset{˙}{]} ((c \in ℝ \land 1 < c) \land i = [1, c)) \to \underset{˙}{[} [1, c) / i \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.)))$
177	174 176	mpbi	$⊢ \underset{˙}{[} [1, c) / i \underset{˙}{]} ((c \in ℝ \land 1 < c) \land i = [1, c)) \to \underset{˙}{[} [1, c) / i \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.))$
178		sbcan	$⊢ \underset{˙}{[} [1, c) / i \underset{˙}{]} ((c \in ℝ \land 1 < c) \land i = [1, c)) \leftrightarrow (\underset{˙}{[} [1, c) / i \underset{˙}{]} (c \in ℝ \land 1 < c) \land \underset{˙}{[} [1, c) / i \underset{˙}{]} i = [1, c))$
179		eqid	$⊢ [1, c) = [1, c)$
180		eqsbc1	$⊢ [1, c) \in V \to (\underset{˙}{[} [1, c) / i \underset{˙}{]} i = [1, c) \leftrightarrow [1, c) = [1, c))$
181	5 180	ax-mp	$⊢ \underset{˙}{[} [1, c) / i \underset{˙}{]} i = [1, c) \leftrightarrow [1, c) = [1, c)$
182	179 181	mpbir	$⊢ \underset{˙}{[} [1, c) / i \underset{˙}{]} i = [1, c)$
183		sbcg	$⊢ [1, c) \in V \to (\underset{˙}{[} [1, c) / i \underset{˙}{]} (c \in ℝ \land 1 < c) \leftrightarrow (c \in ℝ \land 1 < c))$
184	5 183	ax-mp	$⊢ \underset{˙}{[} [1, c) / i \underset{˙}{]} (c \in ℝ \land 1 < c) \leftrightarrow (c \in ℝ \land 1 < c)$
185	184	anbi1i	$⊢ (\underset{˙}{[} [1, c) / i \underset{˙}{]} (c \in ℝ \land 1 < c) \land \underset{˙}{[} [1, c) / i \underset{˙}{]} i = [1, c)) \leftrightarrow ((c \in ℝ \land 1 < c) \land \underset{˙}{[} [1, c) / i \underset{˙}{]} i = [1, c))$
186	182 185	mpbiran2	$⊢ (\underset{˙}{[} [1, c) / i \underset{˙}{]} (c \in ℝ \land 1 < c) \land \underset{˙}{[} [1, c) / i \underset{˙}{]} i = [1, c)) \leftrightarrow (c \in ℝ \land 1 < c)$
187	178 186	bitri	$⊢ \underset{˙}{[} [1, c) / i \underset{˙}{]} ((c \in ℝ \land 1 < c) \land i = [1, c)) \leftrightarrow (c \in ℝ \land 1 < c)$
188		sbcg	$⊢ [1, c) \in V \to (\underset{˙}{[} [1, c) / i \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.)) \leftrightarrow \neg topGen (I) \subseteq topGen (ran (.)))$
189	5 188	ax-mp	$⊢ \underset{˙}{[} [1, c) / i \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.)) \leftrightarrow \neg topGen (I) \subseteq topGen (ran (.))$
190	177 187 189	3imtr3i	$⊢ (c \in ℝ \land 1 < c) \to \neg topGen (I) \subseteq topGen (ran (.))$
191	190	sbcth	$⊢ 2 \in ℝ \to \underset{˙}{[} 2 / c \underset{˙}{]} ((c \in ℝ \land 1 < c) \to \neg topGen (I) \subseteq topGen (ran (.)))$
192	3 191	ax-mp	$⊢ \underset{˙}{[} 2 / c \underset{˙}{]} ((c \in ℝ \land 1 < c) \to \neg topGen (I) \subseteq topGen (ran (.)))$
193		sbcimg	$⊢ 2 \in ℝ \to (\underset{˙}{[} 2 / c \underset{˙}{]} ((c \in ℝ \land 1 < c) \to \neg topGen (I) \subseteq topGen (ran (.))) \leftrightarrow (\underset{˙}{[} 2 / c \underset{˙}{]} (c \in ℝ \land 1 < c) \to \underset{˙}{[} 2 / c \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.))))$
194	3 193	ax-mp	$⊢ \underset{˙}{[} 2 / c \underset{˙}{]} ((c \in ℝ \land 1 < c) \to \neg topGen (I) \subseteq topGen (ran (.))) \leftrightarrow (\underset{˙}{[} 2 / c \underset{˙}{]} (c \in ℝ \land 1 < c) \to \underset{˙}{[} 2 / c \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.)))$
195	192 194	mpbi	$⊢ \underset{˙}{[} 2 / c \underset{˙}{]} (c \in ℝ \land 1 < c) \to \underset{˙}{[} 2 / c \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.))$
196		sbcan	$⊢ \underset{˙}{[} 2 / c \underset{˙}{]} (c \in ℝ \land 1 < c) \leftrightarrow (\underset{˙}{[} 2 / c \underset{˙}{]} c \in ℝ \land \underset{˙}{[} 2 / c \underset{˙}{]} 1 < c)$
197		sbcel1v	$⊢ \underset{˙}{[} 2 / c \underset{˙}{]} c \in ℝ \leftrightarrow 2 \in ℝ$
198		sbcbr123	$⊢ \underset{˙}{[} 2 / c \underset{˙}{]} 1 < c \leftrightarrow ⦋ 2 / c ⦌ 1 ⦋ 2 / c ⦌ < ⦋ 2 / c ⦌ c$
199		csbconstg	$⊢ 2 \in ℝ \to ⦋ 2 / c ⦌ 1 = 1$
200	3 199	ax-mp	$⊢ ⦋ 2 / c ⦌ 1 = 1$
201		csbvarg	$⊢ 2 \in ℝ \to ⦋ 2 / c ⦌ c = 2$
202	3 201	ax-mp	$⊢ ⦋ 2 / c ⦌ c = 2$
203	200 202	breq12i	$⊢ ⦋ 2 / c ⦌ 1 ⦋ 2 / c ⦌ < ⦋ 2 / c ⦌ c \leftrightarrow 1 ⦋ 2 / c ⦌ < 2$
204		csbconstg	$⊢ 2 \in ℝ \to ⦋ 2 / c ⦌ < = <$
205	3 204	ax-mp	$⊢ ⦋ 2 / c ⦌ < = <$
206	205	breqi	$⊢ 1 ⦋ 2 / c ⦌ < 2 \leftrightarrow 1 < 2$
207	198 203 206	3bitri	$⊢ \underset{˙}{[} 2 / c \underset{˙}{]} 1 < c \leftrightarrow 1 < 2$
208	197 207	anbi12i	$⊢ (\underset{˙}{[} 2 / c \underset{˙}{]} c \in ℝ \land \underset{˙}{[} 2 / c \underset{˙}{]} 1 < c) \leftrightarrow (2 \in ℝ \land 1 < 2)$
209	196 208	bitri	$⊢ \underset{˙}{[} 2 / c \underset{˙}{]} (c \in ℝ \land 1 < c) \leftrightarrow (2 \in ℝ \land 1 < 2)$
210		sbcg	$⊢ 2 \in ℝ \to (\underset{˙}{[} 2 / c \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.)) \leftrightarrow \neg topGen (I) \subseteq topGen (ran (.)))$
211	3 210	ax-mp	$⊢ \underset{˙}{[} 2 / c \underset{˙}{]} \neg topGen (I) \subseteq topGen (ran (.)) \leftrightarrow \neg topGen (I) \subseteq topGen (ran (.))$
212	195 209 211	3imtr3i	$⊢ (2 \in ℝ \land 1 < 2) \to \neg topGen (I) \subseteq topGen (ran (.))$
213	3 4 212	mp2an	$⊢ \neg topGen (I) \subseteq topGen (ran (.))$
214		eqimss	$⊢ topGen (I) = topGen (ran (.)) \to topGen (I) \subseteq topGen (ran (.))$
215	213 214	mto	$⊢ \neg topGen (I) = topGen (ran (.))$
216	215	nesymir	$⊢ topGen (ran (.)) \neq topGen (I)$
217		df-pss	$⊢ topGen (ran (.)) \subset topGen (I) \leftrightarrow (topGen (ran (.)) \subseteq topGen (I) \land topGen (ran (.)) \neq topGen (I))$
218	2 216 217	mpbir2an	$⊢ topGen (ran (.)) \subset topGen (I)$

Metamath Proof Explorer

Theorem relowlpssretop

Proof