reconnlem2

	Ref	Expression
Hypotheses	reconnlem2.1	$⊢ φ \to A \subseteq ℝ$
	reconnlem2.2	$⊢ φ \to U \in topGen (ran (.))$
	reconnlem2.3	$⊢ φ \to V \in topGen (ran (.))$
	reconnlem2.4	$⊢ φ \to \forall x \in A \forall y \in A [x, y] \subseteq A$
	reconnlem2.5	$⊢ φ \to B \in (U \cap A)$
	reconnlem2.6	$⊢ φ \to C \in (V \cap A)$
	reconnlem2.7	$⊢ φ \to U \cap V \subseteq ℝ ∖ A$
	reconnlem2.8	$⊢ φ \to B \leq C$
	reconnlem2.9	$⊢ S = sup (U \cap [B, C] ℝ <)$
Assertion	reconnlem2	$⊢ φ \to \neg A \subseteq U \cup V$

Proof

Step	Hyp	Ref	Expression
1		reconnlem2.1	$⊢ φ \to A \subseteq ℝ$
2		reconnlem2.2	$⊢ φ \to U \in topGen (ran (.))$
3		reconnlem2.3	$⊢ φ \to V \in topGen (ran (.))$
4		reconnlem2.4	$⊢ φ \to \forall x \in A \forall y \in A [x, y] \subseteq A$
5		reconnlem2.5	$⊢ φ \to B \in (U \cap A)$
6		reconnlem2.6	$⊢ φ \to C \in (V \cap A)$
7		reconnlem2.7	$⊢ φ \to U \cap V \subseteq ℝ ∖ A$
8		reconnlem2.8	$⊢ φ \to B \leq C$
9		reconnlem2.9	$⊢ S = sup (U \cap [B, C] ℝ <)$
10		inss2	$⊢ U \cap [B, C] \subseteq [B, C]$
11	5	elin2d	$⊢ φ \to B \in A$
12	6	elin2d	$⊢ φ \to C \in A$
13		oveq1	$⊢ x = B \to [x, y] = [B, y]$
14	13	sseq1d	$⊢ x = B \to ([x, y] \subseteq A \leftrightarrow [B, y] \subseteq A)$
15		oveq2	$⊢ y = C \to [B, y] = [B, C]$
16	15	sseq1d	$⊢ y = C \to ([B, y] \subseteq A \leftrightarrow [B, C] \subseteq A)$
17	14 16	rspc2va	$⊢ ((B \in A \land C \in A) \land \forall x \in A \forall y \in A [x, y] \subseteq A) \to [B, C] \subseteq A$
18	11 12 4 17	syl21anc	$⊢ φ \to [B, C] \subseteq A$
19	18 1	sstrd	$⊢ φ \to [B, C] \subseteq ℝ$
20	10 19	sstrid	$⊢ φ \to U \cap [B, C] \subseteq ℝ$
21	5	elin1d	$⊢ φ \to B \in U$
22	1 11	sseldd	$⊢ φ \to B \in ℝ$
23	22	rexrd	$⊢ φ \to B \in ℝ^{*}$
24	1 12	sseldd	$⊢ φ \to C \in ℝ$
25	24	rexrd	$⊢ φ \to C \in ℝ^{*}$
26		lbicc2	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B \leq C) \to B \in [B, C]$
27	23 25 8 26	syl3anc	$⊢ φ \to B \in [B, C]$
28	21 27	elind	$⊢ φ \to B \in (U \cap [B, C])$
29	28	ne0d	$⊢ φ \to U \cap [B, C] \neq \emptyset$
30		elinel2	$⊢ w \in (U \cap [B, C]) \to w \in [B, C]$
31		elicc2	$⊢ (B \in ℝ \land C \in ℝ) \to (w \in [B, C] \leftrightarrow (w \in ℝ \land B \leq w \land w \leq C))$
32	22 24 31	syl2anc	$⊢ φ \to (w \in [B, C] \leftrightarrow (w \in ℝ \land B \leq w \land w \leq C))$
33		simp3	$⊢ (w \in ℝ \land B \leq w \land w \leq C) \to w \leq C$
34	32 33	syl6bi	$⊢ φ \to (w \in [B, C] \to w \leq C)$
35	30 34	syl5	$⊢ φ \to (w \in (U \cap [B, C]) \to w \leq C)$
36	35	ralrimiv	$⊢ φ \to \forall w \in (U \cap [B, C]) w \leq C$
37		brralrspcev	$⊢ (C \in ℝ \land \forall w \in (U \cap [B, C]) w \leq C) \to \exists z \in ℝ \forall w \in (U \cap [B, C]) w \leq z$
38	24 36 37	syl2anc	$⊢ φ \to \exists z \in ℝ \forall w \in (U \cap [B, C]) w \leq z$
39	20 29 38	suprcld	$⊢ φ \to sup (U \cap [B, C] ℝ <) \in ℝ$
40	9 39	eqeltrid	$⊢ φ \to S \in ℝ$
41		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
42		ltaddrp	$⊢ (S \in ℝ \land \frac{r}{2} \in ℝ^{+}) \to S < S + (\frac{r}{2})$
43	40 41 42	syl2an	$⊢ (φ \land r \in ℝ^{+}) \to S < S + (\frac{r}{2})$
44	40	adantr	$⊢ (φ \land r \in ℝ^{+}) \to S \in ℝ$
45	41	rpred	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ$
46		readdcl	$⊢ (S \in ℝ \land \frac{r}{2} \in ℝ) \to S + (\frac{r}{2}) \in ℝ$
47	40 45 46	syl2an	$⊢ (φ \land r \in ℝ^{+}) \to S + (\frac{r}{2}) \in ℝ$
48	44 47	ltnled	$⊢ (φ \land r \in ℝ^{+}) \to (S < S + (\frac{r}{2}) \leftrightarrow \neg S + (\frac{r}{2}) \leq S)$
49	43 48	mpbid	$⊢ (φ \land r \in ℝ^{+}) \to \neg S + (\frac{r}{2}) \leq S$
50	20	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to U \cap [B, C] \subseteq ℝ$
51	29	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to U \cap [B, C] \neq \emptyset$
52	38	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to \exists z \in ℝ \forall w \in (U \cap [B, C]) w \leq z$
53		simpr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) \in (U \cap (−∞, C))$
54	53	elin1d	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) \in U$
55	47	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) \in ℝ$
56	22	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to B \in ℝ$
57	40	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S \in ℝ$
58	20 29 38 28	suprubd	$⊢ φ \to B \leq sup (U \cap [B, C] ℝ <)$
59	58 9	breqtrrdi	$⊢ φ \to B \leq S$
60	59	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to B \leq S$
61	43	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S < S + (\frac{r}{2})$
62	57 55 61	ltled	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S \leq S + (\frac{r}{2})$
63	56 57 55 60 62	letrd	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to B \leq S + (\frac{r}{2})$
64	24	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to C \in ℝ$
65	53	elin2d	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) \in (−∞, C)$
66		eliooord	$⊢ S + (\frac{r}{2}) \in (−∞, C) \to (−∞ < S + (\frac{r}{2}) \land S + (\frac{r}{2}) < C)$
67	66	simprd	$⊢ S + (\frac{r}{2}) \in (−∞, C) \to S + (\frac{r}{2}) < C$
68	65 67	syl	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) < C$
69	55 64 68	ltled	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) \leq C$
70		elicc2	$⊢ (B \in ℝ \land C \in ℝ) \to (S + (\frac{r}{2}) \in [B, C] \leftrightarrow (S + (\frac{r}{2}) \in ℝ \land B \leq S + (\frac{r}{2}) \land S + (\frac{r}{2}) \leq C))$
71	56 64 70	syl2anc	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to (S + (\frac{r}{2}) \in [B, C] \leftrightarrow (S + (\frac{r}{2}) \in ℝ \land B \leq S + (\frac{r}{2}) \land S + (\frac{r}{2}) \leq C))$
72	55 63 69 71	mpbir3and	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) \in [B, C]$
73	54 72	elind	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) \in (U \cap [B, C])$
74	50 51 52 73	suprubd	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) \leq sup (U \cap [B, C] ℝ <)$
75	74 9	breqtrrdi	$⊢ ((φ \land r \in ℝ^{+}) \land S + (\frac{r}{2}) \in (U \cap (−∞, C))) \to S + (\frac{r}{2}) \leq S$
76	49 75	mtand	$⊢ (φ \land r \in ℝ^{+}) \to \neg S + (\frac{r}{2}) \in (U \cap (−∞, C))$
77		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
78	77	remetdval	$⊢ (S + (\frac{r}{2}) \in ℝ \land S \in ℝ) \to (S + (\frac{r}{2})) ({(abs \circ -) ↾}_{ℝ^{2}}) S = \|S + (\frac{r}{2}) - S\|$
79	47 44 78	syl2anc	$⊢ (φ \land r \in ℝ^{+}) \to (S + (\frac{r}{2})) ({(abs \circ -) ↾}_{ℝ^{2}}) S = \|S + (\frac{r}{2}) - S\|$
80	44	recnd	$⊢ (φ \land r \in ℝ^{+}) \to S \in ℂ$
81	45	adantl	$⊢ (φ \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ$
82	81	recnd	$⊢ (φ \land r \in ℝ^{+}) \to \frac{r}{2} \in ℂ$
83	80 82	pncan2d	$⊢ (φ \land r \in ℝ^{+}) \to S + (\frac{r}{2}) - S = \frac{r}{2}$
84	83	fveq2d	$⊢ (φ \land r \in ℝ^{+}) \to \|S + (\frac{r}{2}) - S\| = \|\frac{r}{2}\|$
85	41	adantl	$⊢ (φ \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ^{+}$
86		rpre	$⊢ \frac{r}{2} \in ℝ^{+} \to \frac{r}{2} \in ℝ$
87		rpge0	$⊢ \frac{r}{2} \in ℝ^{+} \to 0 \leq \frac{r}{2}$
88	86 87	absidd	$⊢ \frac{r}{2} \in ℝ^{+} \to \|\frac{r}{2}\| = \frac{r}{2}$
89	85 88	syl	$⊢ (φ \land r \in ℝ^{+}) \to \|\frac{r}{2}\| = \frac{r}{2}$
90	79 84 89	3eqtrd	$⊢ (φ \land r \in ℝ^{+}) \to (S + (\frac{r}{2})) ({(abs \circ -) ↾}_{ℝ^{2}}) S = \frac{r}{2}$
91		rphalflt	$⊢ r \in ℝ^{+} \to \frac{r}{2} < r$
92	91	adantl	$⊢ (φ \land r \in ℝ^{+}) \to \frac{r}{2} < r$
93	90 92	eqbrtrd	$⊢ (φ \land r \in ℝ^{+}) \to (S + (\frac{r}{2})) ({(abs \circ -) ↾}_{ℝ^{2}}) S < r$
94	77	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
95	94	a1i	$⊢ (φ \land r \in ℝ^{+}) \to {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
96		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
97	96	adantl	$⊢ (φ \land r \in ℝ^{+}) \to r \in ℝ^{*}$
98		elbl3	$⊢ (({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land r \in ℝ^{*}) \land (S \in ℝ \land S + (\frac{r}{2}) \in ℝ)) \to (S + (\frac{r}{2}) \in (S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r) \leftrightarrow (S + (\frac{r}{2})) ({(abs \circ -) ↾}_{ℝ^{2}}) S < r)$
99	95 97 44 47 98	syl22anc	$⊢ (φ \land r \in ℝ^{+}) \to (S + (\frac{r}{2}) \in (S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r) \leftrightarrow (S + (\frac{r}{2})) ({(abs \circ -) ↾}_{ℝ^{2}}) S < r)$
100	93 99	mpbird	$⊢ (φ \land r \in ℝ^{+}) \to S + (\frac{r}{2}) \in (S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r)$
101		ssel	$⊢ S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C) \to (S + (\frac{r}{2}) \in (S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r) \to S + (\frac{r}{2}) \in (U \cap (−∞, C)))$
102	100 101	syl5com	$⊢ (φ \land r \in ℝ^{+}) \to (S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C) \to S + (\frac{r}{2}) \in (U \cap (−∞, C)))$
103	76 102	mtod	$⊢ (φ \land r \in ℝ^{+}) \to \neg S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C)$
104	103	nrexdv	$⊢ φ \to \neg \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C)$
105	40	adantr	$⊢ (φ \land S \in U) \to S \in ℝ$
106	105	mnfltd	$⊢ (φ \land S \in U) \to −∞ < S$
107		suprleub	$⊢ ((U \cap [B, C] \subseteq ℝ \land U \cap [B, C] \neq \emptyset \land \exists z \in ℝ \forall w \in (U \cap [B, C]) w \leq z) \land C \in ℝ) \to (sup (U \cap [B, C] ℝ <) \leq C \leftrightarrow \forall w \in (U \cap [B, C]) w \leq C)$
108	20 29 38 24 107	syl31anc	$⊢ φ \to (sup (U \cap [B, C] ℝ <) \leq C \leftrightarrow \forall w \in (U \cap [B, C]) w \leq C)$
109	36 108	mpbird	$⊢ φ \to sup (U \cap [B, C] ℝ <) \leq C$
110	9 109	eqbrtrid	$⊢ φ \to S \leq C$
111	40 24	leloed	$⊢ φ \to (S \leq C \leftrightarrow (S < C \lor S = C))$
112	110 111	mpbid	$⊢ φ \to (S < C \lor S = C)$
113	112	ord	$⊢ φ \to (\neg S < C \to S = C)$
114		elndif	$⊢ C \in A \to \neg C \in (ℝ ∖ A)$
115	12 114	syl	$⊢ φ \to \neg C \in (ℝ ∖ A)$
116	6	elin1d	$⊢ φ \to C \in V$
117		elin	$⊢ C \in (U \cap V) \leftrightarrow (C \in U \land C \in V)$
118	7	sseld	$⊢ φ \to (C \in (U \cap V) \to C \in (ℝ ∖ A))$
119	117 118	biimtrrid	$⊢ φ \to ((C \in U \land C \in V) \to C \in (ℝ ∖ A))$
120	116 119	mpan2d	$⊢ φ \to (C \in U \to C \in (ℝ ∖ A))$
121	115 120	mtod	$⊢ φ \to \neg C \in U$
122		eleq1	$⊢ S = C \to (S \in U \leftrightarrow C \in U)$
123	122	notbid	$⊢ S = C \to (\neg S \in U \leftrightarrow \neg C \in U)$
124	121 123	syl5ibrcom	$⊢ φ \to (S = C \to \neg S \in U)$
125	113 124	syld	$⊢ φ \to (\neg S < C \to \neg S \in U)$
126	125	con4d	$⊢ φ \to (S \in U \to S < C)$
127	126	imp	$⊢ (φ \land S \in U) \to S < C$
128		mnfxr	$⊢ −∞ \in ℝ^{*}$
129		elioo2	$⊢ (−∞ \in ℝ^{} \land C \in ℝ^{}) \to (S \in (−∞, C) \leftrightarrow (S \in ℝ \land −∞ < S \land S < C))$
130	128 25 129	sylancr	$⊢ φ \to (S \in (−∞, C) \leftrightarrow (S \in ℝ \land −∞ < S \land S < C))$
131	130	adantr	$⊢ (φ \land S \in U) \to (S \in (−∞, C) \leftrightarrow (S \in ℝ \land −∞ < S \land S < C))$
132	105 106 127 131	mpbir3and	$⊢ (φ \land S \in U) \to S \in (−∞, C)$
133	132	ex	$⊢ φ \to (S \in U \to S \in (−∞, C))$
134	133	ancld	$⊢ φ \to (S \in U \to (S \in U \land S \in (−∞, C)))$
135		elin	$⊢ S \in (U \cap (−∞, C)) \leftrightarrow (S \in U \land S \in (−∞, C))$
136		retop	$⊢ topGen (ran (.)) \in Top$
137		iooretop	$⊢ (−∞, C) \in topGen (ran (.))$
138		inopn	$⊢ (topGen (ran (.)) \in Top \land U \in topGen (ran (.)) \land (−∞, C) \in topGen (ran (.))) \to U \cap (−∞, C) \in topGen (ran (.))$
139	136 137 138	mp3an13	$⊢ U \in topGen (ran (.)) \to U \cap (−∞, C) \in topGen (ran (.))$
140		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
141	77 140	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
142	141	mopni2	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land U \cap (−∞, C) \in topGen (ran (.)) \land S \in (U \cap (−∞, C))) \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C)$
143	94 142	mp3an1	$⊢ (U \cap (−∞, C) \in topGen (ran (.)) \land S \in (U \cap (−∞, C))) \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C)$
144	143	ex	$⊢ U \cap (−∞, C) \in topGen (ran (.)) \to (S \in (U \cap (−∞, C)) \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C))$
145	2 139 144	3syl	$⊢ φ \to (S \in (U \cap (−∞, C)) \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C))$
146	135 145	biimtrrid	$⊢ φ \to ((S \in U \land S \in (−∞, C)) \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C))$
147	134 146	syld	$⊢ φ \to (S \in U \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq U \cap (−∞, C))$
148	104 147	mtod	$⊢ φ \to \neg S \in U$
149		ltsubrp	$⊢ (S \in ℝ \land r \in ℝ^{+}) \to S - r < S$
150	40 149	sylan	$⊢ (φ \land r \in ℝ^{+}) \to S - r < S$
151		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
152		resubcl	$⊢ (S \in ℝ \land r \in ℝ) \to S - r \in ℝ$
153	40 151 152	syl2an	$⊢ (φ \land r \in ℝ^{+}) \to S - r \in ℝ$
154	153 44	ltnled	$⊢ (φ \land r \in ℝ^{+}) \to (S - r < S \leftrightarrow \neg S \leq S - r)$
155	150 154	mpbid	$⊢ (φ \land r \in ℝ^{+}) \to \neg S \leq S - r$
156	77	bl2ioo	$⊢ (S \in ℝ \land r \in ℝ) \to S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (S - r, S + r)$
157	40 151 156	syl2an	$⊢ (φ \land r \in ℝ^{+}) \to S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r = (S - r, S + r)$
158	157	sseq1d	$⊢ (φ \land r \in ℝ^{+}) \to (S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq V \leftrightarrow (S - r, S + r) \subseteq V)$
159	20	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land w \in (U \cap [B, C])) \to U \cap [B, C] \subseteq ℝ$
160		simpr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land w \in (U \cap [B, C])) \to w \in (U \cap [B, C])$
161	159 160	sseldd	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land w \in (U \cap [B, C])) \to w \in ℝ$
162	153	ad2antrr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land w \in (U \cap [B, C])) \to S - r \in ℝ$
163	18	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to [B, C] \subseteq A$
164	10 163	sstrid	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to U \cap [B, C] \subseteq A$
165	164	sselda	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land w \in (U \cap [B, C])) \to w \in A$
166		elndif	$⊢ w \in A \to \neg w \in (ℝ ∖ A)$
167	165 166	syl	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land w \in (U \cap [B, C])) \to \neg w \in (ℝ ∖ A)$
168	7	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to U \cap V \subseteq ℝ ∖ A$
169		simprl	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w \in (U \cap [B, C])$
170	169	elin1d	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w \in U$
171		simplr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to (S - r, S + r) \subseteq V$
172	161	adantrr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w \in ℝ$
173		simprr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to S - r < w$
174	44	ad2antrr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to S \in ℝ$
175		simpllr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to r \in ℝ^{+}$
176	175	rpred	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to r \in ℝ$
177	174 176	readdcld	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to S + r \in ℝ$
178	159	adantrr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to U \cap [B, C] \subseteq ℝ$
179	29	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to U \cap [B, C] \neq \emptyset$
180	38	ad3antrrr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to \exists z \in ℝ \forall w \in (U \cap [B, C]) w \leq z$
181	178 179 180 169	suprubd	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w \leq sup (U \cap [B, C] ℝ <)$
182	181 9	breqtrrdi	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w \leq S$
183	174 175	ltaddrpd	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to S < S + r$
184	172 174 177 182 183	lelttrd	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w < S + r$
185	153	ad2antrr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to S - r \in ℝ$
186		rexr	$⊢ S - r \in ℝ \to S - r \in ℝ^{*}$
187		rexr	$⊢ S + r \in ℝ \to S + r \in ℝ^{*}$
188		elioo2	$⊢ (S - r \in ℝ^{} \land S + r \in ℝ^{}) \to (w \in (S - r, S + r) \leftrightarrow (w \in ℝ \land S - r < w \land w < S + r))$
189	186 187 188	syl2an	$⊢ (S - r \in ℝ \land S + r \in ℝ) \to (w \in (S - r, S + r) \leftrightarrow (w \in ℝ \land S - r < w \land w < S + r))$
190	185 177 189	syl2anc	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to (w \in (S - r, S + r) \leftrightarrow (w \in ℝ \land S - r < w \land w < S + r))$
191	172 173 184 190	mpbir3and	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w \in (S - r, S + r)$
192	171 191	sseldd	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w \in V$
193	170 192	elind	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w \in (U \cap V)$
194	168 193	sseldd	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land (w \in (U \cap [B, C]) \land S - r < w)) \to w \in (ℝ ∖ A)$
195	194	expr	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land w \in (U \cap [B, C])) \to (S - r < w \to w \in (ℝ ∖ A))$
196	167 195	mtod	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land w \in (U \cap [B, C])) \to \neg S - r < w$
197	161 162 196	nltled	$⊢ (((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \land w \in (U \cap [B, C])) \to w \leq S - r$
198	197	ralrimiva	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to \forall w \in (U \cap [B, C]) w \leq S - r$
199	20	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to U \cap [B, C] \subseteq ℝ$
200	29	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to U \cap [B, C] \neq \emptyset$
201	38	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to \exists z \in ℝ \forall w \in (U \cap [B, C]) w \leq z$
202	153	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to S - r \in ℝ$
203		suprleub	$⊢ ((U \cap [B, C] \subseteq ℝ \land U \cap [B, C] \neq \emptyset \land \exists z \in ℝ \forall w \in (U \cap [B, C]) w \leq z) \land S - r \in ℝ) \to (sup (U \cap [B, C] ℝ <) \leq S - r \leftrightarrow \forall w \in (U \cap [B, C]) w \leq S - r)$
204	199 200 201 202 203	syl31anc	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to (sup (U \cap [B, C] ℝ <) \leq S - r \leftrightarrow \forall w \in (U \cap [B, C]) w \leq S - r)$
205	198 204	mpbird	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to sup (U \cap [B, C] ℝ <) \leq S - r$
206	9 205	eqbrtrid	$⊢ ((φ \land r \in ℝ^{+}) \land (S - r, S + r) \subseteq V) \to S \leq S - r$
207	206	ex	$⊢ (φ \land r \in ℝ^{+}) \to ((S - r, S + r) \subseteq V \to S \leq S - r)$
208	158 207	sylbid	$⊢ (φ \land r \in ℝ^{+}) \to (S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq V \to S \leq S - r)$
209	155 208	mtod	$⊢ (φ \land r \in ℝ^{+}) \to \neg S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq V$
210	209	nrexdv	$⊢ φ \to \neg \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq V$
211	141	mopni2	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land V \in topGen (ran (.)) \land S \in V) \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq V$
212	94 211	mp3an1	$⊢ (V \in topGen (ran (.)) \land S \in V) \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq V$
213	212	ex	$⊢ V \in topGen (ran (.)) \to (S \in V \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq V)$
214	3 213	syl	$⊢ φ \to (S \in V \to \exists r \in ℝ^{+} S ball ({(abs \circ -) ↾}_{ℝ^{2}}) r \subseteq V)$
215	210 214	mtod	$⊢ φ \to \neg S \in V$
216		ioran	$⊢ \neg (S \in U \lor S \in V) \leftrightarrow (\neg S \in U \land \neg S \in V)$
217	148 215 216	sylanbrc	$⊢ φ \to \neg (S \in U \lor S \in V)$
218		elun	$⊢ S \in (U \cup V) \leftrightarrow (S \in U \lor S \in V)$
219	217 218	sylnibr	$⊢ φ \to \neg S \in (U \cup V)$
220		elicc2	$⊢ (B \in ℝ \land C \in ℝ) \to (S \in [B, C] \leftrightarrow (S \in ℝ \land B \leq S \land S \leq C))$
221	22 24 220	syl2anc	$⊢ φ \to (S \in [B, C] \leftrightarrow (S \in ℝ \land B \leq S \land S \leq C))$
222	40 59 110 221	mpbir3and	$⊢ φ \to S \in [B, C]$
223	18 222	sseldd	$⊢ φ \to S \in A$
224		ssel	$⊢ A \subseteq U \cup V \to (S \in A \to S \in (U \cup V))$
225	223 224	syl5com	$⊢ φ \to (A \subseteq U \cup V \to S \in (U \cup V))$
226	219 225	mtod	$⊢ φ \to \neg A \subseteq U \cup V$

Metamath Proof Explorer

Theorem reconnlem2

Proof