Theorem metnrmlem3

Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 5-Sep-2015)

	Ref	Expression
Hypotheses	metdscn.f	$$⊢F=\left(x\in X⟼sup\left(\mathrm{ran}\left(y\in S⟼xDy\right),{ℝ}^{*},<\right)\right)$$
	metdscn.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
	metnrmlem.1	$$⊢\phi \to D\in \mathrm{\infty Met}\left(X\right)$$
	metnrmlem.2	$$⊢\phi \to S\in \mathrm{Clsd}\left(J\right)$$
	metnrmlem.3	$$⊢\phi \to T\in \mathrm{Clsd}\left(J\right)$$
	metnrmlem.4	$$⊢\phi \to S\cap T=\varnothing$$
	metnrmlem.u	$$⊢U=\bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
	metnrmlem.g	$$⊢G=\left(x\in X⟼sup\left(\mathrm{ran}\left(y\in T⟼xDy\right),{ℝ}^{*},<\right)\right)$$
	metnrmlem.v	$$⊢V=\bigcup _{s\in S}\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)$$
Assertion	metnrmlem3	$$⊢\phi \to \exists z\in J\exists w\in J\left(S\subseteq z\wedge T\subseteq w\wedge z\cap w=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$$⊢F=\left(x\in X⟼sup\left(\mathrm{ran}\left(y\in S⟼xDy\right),{ℝ}^{*},<\right)\right)$$
2		metdscn.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
3		metnrmlem.1	$$⊢\phi \to D\in \mathrm{\infty Met}\left(X\right)$$
4		metnrmlem.2	$$⊢\phi \to S\in \mathrm{Clsd}\left(J\right)$$
5		metnrmlem.3	$$⊢\phi \to T\in \mathrm{Clsd}\left(J\right)$$
6		metnrmlem.4	$$⊢\phi \to S\cap T=\varnothing$$
7		metnrmlem.u	$$⊢U=\bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
8		metnrmlem.g	$$⊢G=\left(x\in X⟼sup\left(\mathrm{ran}\left(y\in T⟼xDy\right),{ℝ}^{*},<\right)\right)$$
9		metnrmlem.v	$$⊢V=\bigcup _{s\in S}\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)$$
10		incom	$$⊢T\cap S=S\cap T$$
11	10 6	syl5eq	$$⊢\phi \to T\cap S=\varnothing$$
12	8 2 3 5 4 11 9	metnrmlem2	$$⊢\phi \to \left(V\in J\wedge S\subseteq V\right)$$
13	12	simpld	$$⊢\phi \to V\in J$$
14	1 2 3 4 5 6 7	metnrmlem2	$$⊢\phi \to \left(U\in J\wedge T\subseteq U\right)$$
15	14	simpld	$$⊢\phi \to U\in J$$
16	12	simprd	$$⊢\phi \to S\subseteq V$$
17	14	simprd	$$⊢\phi \to T\subseteq U$$
18	9	ineq1i	$$⊢V\cap U=\bigcup _{s\in S}\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U$$
19		iunin1	$$⊢\bigcup _{s\in S}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\right)=\bigcup _{s\in S}\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U$$
20	18 19	eqtr4i	$$⊢V\cap U=\bigcup _{s\in S}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\right)$$
21	7	ineq2i	$$⊢\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U=\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
22		iunin2	$$⊢\bigcup _{t\in T}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\right)=\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
23	21 22	eqtr4i	$$⊢\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U=\bigcup _{t\in T}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\right)$$
24	3	adantr	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to D\in \mathrm{\infty Met}\left(X\right)$$
25		eqid	$$⊢\bigcup J=\bigcup J$$
26	25	cldss	$$⊢S\in \mathrm{Clsd}\left(J\right)\to S\subseteq \bigcup J$$
27	4 26	syl	$$⊢\phi \to S\subseteq \bigcup J$$
28	2	mopnuni	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X=\bigcup J$$
29	3 28	syl	$$⊢\phi \to X=\bigcup J$$
30	27 29	sseqtrrd	$$⊢\phi \to S\subseteq X$$
31	30	sselda	$$⊢\left(\phi \wedge s\in S\right)\to s\in X$$
32	31	adantrr	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to s\in X$$
33	25	cldss	$$⊢T\in \mathrm{Clsd}\left(J\right)\to T\subseteq \bigcup J$$
34	5 33	syl	$$⊢\phi \to T\subseteq \bigcup J$$
35	34 29	sseqtrrd	$$⊢\phi \to T\subseteq X$$
36	35	sselda	$$⊢\left(\phi \wedge t\in T\right)\to t\in X$$
37	36	adantrl	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to t\in X$$
38	8 2 3 5 4 11	metnrmlem1a	$$⊢\left(\phi \wedge s\in S\right)\to \left(0<G\left(s\right)\wedge if\left(1\le G\left(s\right),1,G\left(s\right)\right)\in {ℝ}^{+}\right)$$
39	38	simprd	$$⊢\left(\phi \wedge s\in S\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)\in {ℝ}^{+}$$
40	39	adantrr	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)\in {ℝ}^{+}$$
41	40	rphalfcld	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\in {ℝ}^{+}$$
42	41	rpxrd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\in {ℝ}^{*}$$
43	1 2 3 4 5 6	metnrmlem1a	$$⊢\left(\phi \wedge t\in T\right)\to \left(0<F\left(t\right)\wedge if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in {ℝ}^{+}\right)$$
44	43	adantrl	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \left(0<F\left(t\right)\wedge if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in {ℝ}^{+}\right)$$
45	44	simprd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in {ℝ}^{+}$$
46	45	rphalfcld	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in {ℝ}^{+}$$
47	46	rpxrd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in {ℝ}^{*}$$
48	40	rpred	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)\in ℝ$$
49	48	rehalfcld	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\in ℝ$$
50	45	rpred	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in ℝ$$
51	50	rehalfcld	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in ℝ$$
52	49 51	rexaddd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right){+}_{𝑒}\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)=\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)+\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)$$
53	48	recnd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)\in ℂ$$
54	50	recnd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in ℂ$$
55		2cnd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to 2\in ℂ$$
56		2ne0	$$⊢2\ne 0$$
57	56	a1i	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to 2\ne 0$$
58	53 54 55 57	divdird	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}=\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)+\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)$$
59	52 58	eqtr4d	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right){+}_{𝑒}\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)=\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}$$
60	8 2 3 5 4 11	metnrmlem1	$$⊢\left(\phi \wedge \left(t\in T\wedge s\in S\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)\le tDs$$
61	60	ancom2s	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)\le tDs$$
62		xmetsym	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge t\in X\wedge s\in X\right)\to tDs=sDt$$
63	24 37 32 62	syl3anc	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to tDs=sDt$$
64	61 63	breqtrd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)\le sDt$$
65	1 2 3 4 5 6	metnrmlem1	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le F\left(t\right),1,F\left(t\right)\right)\le sDt$$
66	40	rpxrd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)\in {ℝ}^{*}$$
67	45	rpxrd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in {ℝ}^{*}$$
68		xmetcl	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge s\in X\wedge t\in X\right)\to sDt\in {ℝ}^{*}$$
69	24 32 37 68	syl3anc	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to sDt\in {ℝ}^{*}$$
70		xle2add	$$⊢\left(\left(if\left(1\le G\left(s\right),1,G\left(s\right)\right)\in {ℝ}^{*}\wedge if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in {ℝ}^{*}\right)\wedge \left(sDt\in {ℝ}^{*}\wedge sDt\in {ℝ}^{*}\right)\right)\to \left(\left(if\left(1\le G\left(s\right),1,G\left(s\right)\right)\le sDt\wedge if\left(1\le F\left(t\right),1,F\left(t\right)\right)\le sDt\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right){+}_{𝑒}if\left(1\le F\left(t\right),1,F\left(t\right)\right)\le \left(sDt\right){+}_{𝑒}\left(sDt\right)\right)$$
71	66 67 69 69 70	syl22anc	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \left(\left(if\left(1\le G\left(s\right),1,G\left(s\right)\right)\le sDt\wedge if\left(1\le F\left(t\right),1,F\left(t\right)\right)\le sDt\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right){+}_{𝑒}if\left(1\le F\left(t\right),1,F\left(t\right)\right)\le \left(sDt\right){+}_{𝑒}\left(sDt\right)\right)$$
72	64 65 71	mp2and	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right){+}_{𝑒}if\left(1\le F\left(t\right),1,F\left(t\right)\right)\le \left(sDt\right){+}_{𝑒}\left(sDt\right)$$
73	48 50	readdcld	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in ℝ$$
74	73	recnd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in ℂ$$
75	74 55 57	divcan2d	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to 2\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)=if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)$$
76		2re	$$⊢2\in ℝ$$
77	73	rehalfcld	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in ℝ$$
78		rexmul	$$⊢\left(2\in ℝ\wedge \frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in ℝ\right)\to 2{\cdot }_{𝑒}\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)=2\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)$$
79	76 77 78	sylancr	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to 2{\cdot }_{𝑒}\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)=2\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)$$
80	48 50	rexaddd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to if\left(1\le G\left(s\right),1,G\left(s\right)\right){+}_{𝑒}if\left(1\le F\left(t\right),1,F\left(t\right)\right)=if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)$$
81	75 79 80	3eqtr4d	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to 2{\cdot }_{𝑒}\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)=if\left(1\le G\left(s\right),1,G\left(s\right)\right){+}_{𝑒}if\left(1\le F\left(t\right),1,F\left(t\right)\right)$$
82		x2times	$$⊢sDt\in {ℝ}^{*}\to 2{\cdot }_{𝑒}\left(sDt\right)=\left(sDt\right){+}_{𝑒}\left(sDt\right)$$
83	69 82	syl	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to 2{\cdot }_{𝑒}\left(sDt\right)=\left(sDt\right){+}_{𝑒}\left(sDt\right)$$
84	72 81 83	3brtr4d	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to 2{\cdot }_{𝑒}\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\le 2{\cdot }_{𝑒}\left(sDt\right)$$
85	77	rexrd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in {ℝ}^{*}$$
86		2rp	$$⊢2\in {ℝ}^{+}$$
87	86	a1i	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to 2\in {ℝ}^{+}$$
88		xlemul2	$$⊢\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in {ℝ}^{*}\wedge sDt\in {ℝ}^{*}\wedge 2\in {ℝ}^{+}\right)\to \left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\le sDt\leftrightarrow 2{\cdot }_{𝑒}\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\le 2{\cdot }_{𝑒}\left(sDt\right)\right)$$
89	85 69 87 88	syl3anc	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\le sDt\leftrightarrow 2{\cdot }_{𝑒}\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\le 2{\cdot }_{𝑒}\left(sDt\right)\right)$$
90	84 89	mpbird	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)+if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\le sDt$$
91	59 90	eqbrtrd	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right){+}_{𝑒}\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\le sDt$$
92		bldisj	$$⊢\left(\left(D\in \mathrm{\infty Met}\left(X\right)\wedge s\in X\wedge t\in X\right)\wedge \left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\in {ℝ}^{*}\wedge \frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in {ℝ}^{*}\wedge \left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right){+}_{𝑒}\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\le sDt\right)\right)\to \left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)=\varnothing$$
93	24 32 37 42 47 91 92	syl33anc	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)=\varnothing$$
94		eqimss	$$⊢\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)=\varnothing \to \left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\subseteq \varnothing$$
95	93 94	syl	$$⊢\left(\phi \wedge \left(s\in S\wedge t\in T\right)\right)\to \left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\subseteq \varnothing$$
96	95	anassrs	$$⊢\left(\left(\phi \wedge s\in S\right)\wedge t\in T\right)\to \left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\subseteq \varnothing$$
97	96	ralrimiva	$$⊢\left(\phi \wedge s\in S\right)\to \forall t\in T\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\subseteq \varnothing$$
98		iunss	$$⊢\bigcup _{t\in T}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\right)\subseteq \varnothing \leftrightarrow \forall t\in T\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\subseteq \varnothing$$
99	97 98	sylibr	$$⊢\left(\phi \wedge s\in S\right)\to \bigcup _{t\in T}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\right)\subseteq \varnothing$$
100	23 99	eqsstrid	$$⊢\left(\phi \wedge s\in S\right)\to \left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\subseteq \varnothing$$
101	100	ralrimiva	$$⊢\phi \to \forall s\in S\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\subseteq \varnothing$$
102		iunss	$$⊢\bigcup _{s\in S}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\right)\subseteq \varnothing \leftrightarrow \forall s\in S\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\subseteq \varnothing$$
103	101 102	sylibr	$$⊢\phi \to \bigcup _{s\in S}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\right)\subseteq \varnothing$$
104		ss0	$$⊢\bigcup _{s\in S}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\right)\subseteq \varnothing \to \bigcup _{s\in S}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\right)=\varnothing$$
105	103 104	syl	$$⊢\phi \to \bigcup _{s\in S}\left(\left(s\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le G\left(s\right),1,G\left(s\right)\right)}{2}\right)\right)\cap U\right)=\varnothing$$
106	20 105	syl5eq	$$⊢\phi \to V\cap U=\varnothing$$
107		sseq2	$$⊢z=V\to \left(S\subseteq z\leftrightarrow S\subseteq V\right)$$
108		ineq1	$$⊢z=V\to z\cap w=V\cap w$$
109	108	eqeq1d	$$⊢z=V\to \left(z\cap w=\varnothing \leftrightarrow V\cap w=\varnothing \right)$$
110	107 109	3anbi13d	$$⊢z=V\to \left(\left(S\subseteq z\wedge T\subseteq w\wedge z\cap w=\varnothing \right)\leftrightarrow \left(S\subseteq V\wedge T\subseteq w\wedge V\cap w=\varnothing \right)\right)$$
111		sseq2	$$⊢w=U\to \left(T\subseteq w\leftrightarrow T\subseteq U\right)$$
112		ineq2	$$⊢w=U\to V\cap w=V\cap U$$
113	112	eqeq1d	$$⊢w=U\to \left(V\cap w=\varnothing \leftrightarrow V\cap U=\varnothing \right)$$
114	111 113	3anbi23d	$$⊢w=U\to \left(\left(S\subseteq V\wedge T\subseteq w\wedge V\cap w=\varnothing \right)\leftrightarrow \left(S\subseteq V\wedge T\subseteq U\wedge V\cap U=\varnothing \right)\right)$$
115	110 114	rspc2ev	$$⊢\left(V\in J\wedge U\in J\wedge \left(S\subseteq V\wedge T\subseteq U\wedge V\cap U=\varnothing \right)\right)\to \exists z\in J\exists w\in J\left(S\subseteq z\wedge T\subseteq w\wedge z\cap w=\varnothing \right)$$
116	13 15 16 17 106 115	syl113anc	$$⊢\phi \to \exists z\in J\exists w\in J\left(S\subseteq z\wedge T\subseteq w\wedge z\cap w=\varnothing \right)$$