# Metamath Proof Explorer

## 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}⟼{x}{D}{y}\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}⟼{x}{D}{y}\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}\phantom{\rule{.4em}{0ex}}\exists {w}\in {J}\phantom{\rule{.4em}{0ex}}\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}⟼{x}{D}{y}\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}⟼{x}{D}{y}\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 {t}{D}{s}$
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 {t}{D}{s}$
62 xmetsym ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {t}\in {X}\wedge {s}\in {X}\right)\to {t}{D}{s}={s}{D}{t}$
63 24 37 32 62 syl3anc ${⊢}\left({\phi }\wedge \left({s}\in {S}\wedge {t}\in {T}\right)\right)\to {t}{D}{s}={s}{D}{t}$
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 {s}{D}{t}$
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 {s}{D}{t}$
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 {s}{D}{t}\in {ℝ}^{*}$
69 24 32 37 68 syl3anc ${⊢}\left({\phi }\wedge \left({s}\in {S}\wedge {t}\in {T}\right)\right)\to {s}{D}{t}\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({s}{D}{t}\in {ℝ}^{*}\wedge {s}{D}{t}\in {ℝ}^{*}\right)\right)\to \left(\left(if\left(1\le {G}\left({s}\right),1,{G}\left({s}\right)\right)\le {s}{D}{t}\wedge if\left(1\le {F}\left({t}\right),1,{F}\left({t}\right)\right)\le {s}{D}{t}\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({s}{D}{t}\right){+}_{𝑒}\left({s}{D}{t}\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 {s}{D}{t}\wedge if\left(1\le {F}\left({t}\right),1,{F}\left({t}\right)\right)\le {s}{D}{t}\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({s}{D}{t}\right){+}_{𝑒}\left({s}{D}{t}\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({s}{D}{t}\right){+}_{𝑒}\left({s}{D}{t}\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 ${⊢}{s}{D}{t}\in {ℝ}^{*}\to 2{\cdot }_{𝑒}\left({s}{D}{t}\right)=\left({s}{D}{t}\right){+}_{𝑒}\left({s}{D}{t}\right)$
83 69 82 syl ${⊢}\left({\phi }\wedge \left({s}\in {S}\wedge {t}\in {T}\right)\right)\to 2{\cdot }_{𝑒}\left({s}{D}{t}\right)=\left({s}{D}{t}\right){+}_{𝑒}\left({s}{D}{t}\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({s}{D}{t}\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 {s}{D}{t}\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 {s}{D}{t}↔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({s}{D}{t}\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 {s}{D}{t}↔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({s}{D}{t}\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 {s}{D}{t}$
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 {s}{D}{t}$
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 {s}{D}{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$
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}\phantom{\rule{.4em}{0ex}}\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 ↔\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\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 ↔\forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\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}↔{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 ↔{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)↔\left({S}\subseteq {V}\wedge {T}\subseteq {w}\wedge {V}\cap {w}=\varnothing \right)\right)$
111 sseq2 ${⊢}{w}={U}\to \left({T}\subseteq {w}↔{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 ↔{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)↔\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}\phantom{\rule{.4em}{0ex}}\exists {w}\in {J}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\exists {w}\in {J}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq {z}\wedge {T}\subseteq {w}\wedge {z}\cap {w}=\varnothing \right)$