# Metamath Proof Explorer

## Theorem stoweidlem46

Description: This lemma proves that sets U(t) as defined in Lemma 1 of BrosowskiDeutsh p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem46.1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{U}$
stoweidlem46.2 ${⊢}\underset{_}{Ⅎ}{h}\phantom{\rule{.4em}{0ex}}{Q}$
stoweidlem46.3 ${⊢}Ⅎ{q}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem46.4 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
stoweidlem46.5 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
stoweidlem46.6 ${⊢}{Q}=\left\{{h}\in {A}|\left({h}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right)\right\}$
stoweidlem46.7 ${⊢}{W}=\left\{{w}\in {J}|\exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}{w}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}\right\}$
stoweidlem46.8 ${⊢}{T}=\bigcup {J}$
stoweidlem46.9 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
stoweidlem46.10 ${⊢}{\phi }\to {A}\subseteq {J}\mathrm{Cn}{K}$
stoweidlem46.11 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
stoweidlem46.12 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
stoweidlem46.13 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
stoweidlem46.14 ${⊢}\left({\phi }\wedge \left({r}\in {T}\wedge {t}\in {T}\wedge {r}\ne {t}\right)\right)\to \exists {q}\in {A}\phantom{\rule{.4em}{0ex}}{q}\left({r}\right)\ne {q}\left({t}\right)$
stoweidlem46.15 ${⊢}{\phi }\to {U}\in {J}$
stoweidlem46.16 ${⊢}{\phi }\to {Z}\in {U}$
stoweidlem46.17 ${⊢}{\phi }\to {T}\in \mathrm{V}$
Assertion stoweidlem46 ${⊢}{\phi }\to {T}\setminus {U}\subseteq \bigcup {W}$

### Proof

Step Hyp Ref Expression
1 stoweidlem46.1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{U}$
2 stoweidlem46.2 ${⊢}\underset{_}{Ⅎ}{h}\phantom{\rule{.4em}{0ex}}{Q}$
3 stoweidlem46.3 ${⊢}Ⅎ{q}\phantom{\rule{.4em}{0ex}}{\phi }$
4 stoweidlem46.4 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
5 stoweidlem46.5 ${⊢}{K}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
6 stoweidlem46.6 ${⊢}{Q}=\left\{{h}\in {A}|\left({h}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right)\right\}$
7 stoweidlem46.7 ${⊢}{W}=\left\{{w}\in {J}|\exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}{w}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}\right\}$
8 stoweidlem46.8 ${⊢}{T}=\bigcup {J}$
9 stoweidlem46.9 ${⊢}{\phi }\to {J}\in \mathrm{Comp}$
10 stoweidlem46.10 ${⊢}{\phi }\to {A}\subseteq {J}\mathrm{Cn}{K}$
11 stoweidlem46.11 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
12 stoweidlem46.12 ${⊢}\left({\phi }\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
13 stoweidlem46.13 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
14 stoweidlem46.14 ${⊢}\left({\phi }\wedge \left({r}\in {T}\wedge {t}\in {T}\wedge {r}\ne {t}\right)\right)\to \exists {q}\in {A}\phantom{\rule{.4em}{0ex}}{q}\left({r}\right)\ne {q}\left({t}\right)$
15 stoweidlem46.15 ${⊢}{\phi }\to {U}\in {J}$
16 stoweidlem46.16 ${⊢}{\phi }\to {Z}\in {U}$
17 stoweidlem46.17 ${⊢}{\phi }\to {T}\in \mathrm{V}$
18 nfv ${⊢}Ⅎ{q}\phantom{\rule{.4em}{0ex}}{s}\in \left({T}\setminus {U}\right)$
19 3 18 nfan ${⊢}Ⅎ{q}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)$
20 nfcv ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{T}$
21 20 1 nfdif ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}\left({T}\setminus {U}\right)$
22 21 nfel2 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{s}\in \left({T}\setminus {U}\right)$
23 4 22 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)$
24 9 adantr ${⊢}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\to {J}\in \mathrm{Comp}$
25 10 adantr ${⊢}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\to {A}\subseteq {J}\mathrm{Cn}{K}$
26 11 3adant1r ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right)+{g}\left({t}\right)\right)\in {A}$
27 12 3adant1r ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge {f}\in {A}\wedge {g}\in {A}\right)\to \left({t}\in {T}⟼{f}\left({t}\right){g}\left({t}\right)\right)\in {A}$
28 13 adantlr ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge {x}\in ℝ\right)\to \left({t}\in {T}⟼{x}\right)\in {A}$
29 14 adantlr ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({r}\in {T}\wedge {t}\in {T}\wedge {r}\ne {t}\right)\right)\to \exists {q}\in {A}\phantom{\rule{.4em}{0ex}}{q}\left({r}\right)\ne {q}\left({t}\right)$
30 15 adantr ${⊢}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\to {U}\in {J}$
31 16 adantr ${⊢}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\to {Z}\in {U}$
32 simpr ${⊢}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\to {s}\in \left({T}\setminus {U}\right)$
33 19 23 2 5 6 8 24 25 26 27 28 29 30 31 32 stoweidlem43 ${⊢}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\to \exists {h}\phantom{\rule{.4em}{0ex}}\left({h}\in {Q}\wedge 0<{h}\left({s}\right)\right)$
34 nfv ${⊢}Ⅎ{g}\phantom{\rule{.4em}{0ex}}\left({h}\in {Q}\wedge 0<{h}\left({s}\right)\right)$
35 2 nfel2 ${⊢}Ⅎ{h}\phantom{\rule{.4em}{0ex}}{g}\in {Q}$
36 nfv ${⊢}Ⅎ{h}\phantom{\rule{.4em}{0ex}}0<{g}\left({s}\right)$
37 35 36 nfan ${⊢}Ⅎ{h}\phantom{\rule{.4em}{0ex}}\left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)$
38 eleq1 ${⊢}{h}={g}\to \left({h}\in {Q}↔{g}\in {Q}\right)$
39 fveq1 ${⊢}{h}={g}\to {h}\left({s}\right)={g}\left({s}\right)$
40 39 breq2d ${⊢}{h}={g}\to \left(0<{h}\left({s}\right)↔0<{g}\left({s}\right)\right)$
41 38 40 anbi12d ${⊢}{h}={g}\to \left(\left({h}\in {Q}\wedge 0<{h}\left({s}\right)\right)↔\left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)$
42 34 37 41 cbvexv1 ${⊢}\exists {h}\phantom{\rule{.4em}{0ex}}\left({h}\in {Q}\wedge 0<{h}\left({s}\right)\right)↔\exists {g}\phantom{\rule{.4em}{0ex}}\left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)$
43 33 42 sylib ${⊢}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)$
44 rabexg ${⊢}{T}\in \mathrm{V}\to \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in \mathrm{V}$
45 17 44 syl ${⊢}{\phi }\to \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in \mathrm{V}$
46 45 ad2antrr ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in \mathrm{V}$
47 eldifi ${⊢}{s}\in \left({T}\setminus {U}\right)\to {s}\in {T}$
48 47 ad2antlr ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to {s}\in {T}$
49 simprr ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to 0<{g}\left({s}\right)$
50 fveq2 ${⊢}{t}={s}\to {g}\left({t}\right)={g}\left({s}\right)$
51 50 breq2d ${⊢}{t}={s}\to \left(0<{g}\left({t}\right)↔0<{g}\left({s}\right)\right)$
52 51 elrab ${⊢}{s}\in \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}↔\left({s}\in {T}\wedge 0<{g}\left({s}\right)\right)$
53 48 49 52 sylanbrc ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to {s}\in \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}$
54 simpll ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to {\phi }$
55 10 adantr ${⊢}\left({\phi }\wedge {g}\in {Q}\right)\to {A}\subseteq {J}\mathrm{Cn}{K}$
56 simpr ${⊢}\left({\phi }\wedge {g}\in {Q}\right)\to {g}\in {Q}$
57 56 6 eleqtrdi ${⊢}\left({\phi }\wedge {g}\in {Q}\right)\to {g}\in \left\{{h}\in {A}|\left({h}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right)\right\}$
58 fveq1 ${⊢}{h}={g}\to {h}\left({Z}\right)={g}\left({Z}\right)$
59 58 eqeq1d ${⊢}{h}={g}\to \left({h}\left({Z}\right)=0↔{g}\left({Z}\right)=0\right)$
60 fveq1 ${⊢}{h}={g}\to {h}\left({t}\right)={g}\left({t}\right)$
61 60 breq2d ${⊢}{h}={g}\to \left(0\le {h}\left({t}\right)↔0\le {g}\left({t}\right)\right)$
62 60 breq1d ${⊢}{h}={g}\to \left({h}\left({t}\right)\le 1↔{g}\left({t}\right)\le 1\right)$
63 61 62 anbi12d ${⊢}{h}={g}\to \left(\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)↔\left(0\le {g}\left({t}\right)\wedge {g}\left({t}\right)\le 1\right)\right)$
64 63 ralbidv ${⊢}{h}={g}\to \left(\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)↔\forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {g}\left({t}\right)\wedge {g}\left({t}\right)\le 1\right)\right)$
65 59 64 anbi12d ${⊢}{h}={g}\to \left(\left({h}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right)↔\left({g}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {g}\left({t}\right)\wedge {g}\left({t}\right)\le 1\right)\right)\right)$
66 65 elrab ${⊢}{g}\in \left\{{h}\in {A}|\left({h}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {h}\left({t}\right)\wedge {h}\left({t}\right)\le 1\right)\right)\right\}↔\left({g}\in {A}\wedge \left({g}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {g}\left({t}\right)\wedge {g}\left({t}\right)\le 1\right)\right)\right)$
67 57 66 sylib ${⊢}\left({\phi }\wedge {g}\in {Q}\right)\to \left({g}\in {A}\wedge \left({g}\left({Z}\right)=0\wedge \forall {t}\in {T}\phantom{\rule{.4em}{0ex}}\left(0\le {g}\left({t}\right)\wedge {g}\left({t}\right)\le 1\right)\right)\right)$
68 67 simpld ${⊢}\left({\phi }\wedge {g}\in {Q}\right)\to {g}\in {A}$
69 55 68 sseldd ${⊢}\left({\phi }\wedge {g}\in {Q}\right)\to {g}\in \left({J}\mathrm{Cn}{K}\right)$
70 69 ad2ant2r ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to {g}\in \left({J}\mathrm{Cn}{K}\right)$
71 nfcv ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}0$
72 nfcv ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}{g}$
73 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{g}\in \left({J}\mathrm{Cn}{K}\right)$
74 4 73 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {g}\in \left({J}\mathrm{Cn}{K}\right)\right)$
75 eqid ${⊢}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}$
76 0xr ${⊢}0\in {ℝ}^{*}$
77 76 a1i ${⊢}\left({\phi }\wedge {g}\in \left({J}\mathrm{Cn}{K}\right)\right)\to 0\in {ℝ}^{*}$
78 simpr ${⊢}\left({\phi }\wedge {g}\in \left({J}\mathrm{Cn}{K}\right)\right)\to {g}\in \left({J}\mathrm{Cn}{K}\right)$
79 71 72 74 5 8 75 77 78 rfcnpre1 ${⊢}\left({\phi }\wedge {g}\in \left({J}\mathrm{Cn}{K}\right)\right)\to \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {J}$
80 54 70 79 syl2anc ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {J}$
81 eqidd ${⊢}\left({\phi }\wedge {g}\in {Q}\right)\to \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}$
82 nfv ${⊢}Ⅎ{h}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}$
83 nfcv ${⊢}\underset{_}{Ⅎ}{h}\phantom{\rule{.4em}{0ex}}{g}$
84 60 breq2d ${⊢}{h}={g}\to \left(0<{h}\left({t}\right)↔0<{g}\left({t}\right)\right)$
85 84 rabbidv ${⊢}{h}={g}\to \left\{{t}\in {T}|0<{h}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}$
86 85 eqeq2d ${⊢}{h}={g}\to \left(\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}↔\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\right)$
87 82 83 2 86 rspcegf ${⊢}\left({g}\in {Q}\wedge \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\right)\to \exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}$
88 56 81 87 syl2anc ${⊢}\left({\phi }\wedge {g}\in {Q}\right)\to \exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}$
89 88 ad2ant2r ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to \exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}$
90 eqeq1 ${⊢}{w}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\to \left({w}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}↔\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}\right)$
91 90 rexbidv ${⊢}{w}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\to \left(\exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}{w}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}↔\exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}\right)$
92 91 elrab ${⊢}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in \left\{{w}\in {J}|\exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}{w}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}\right\}↔\left(\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {J}\wedge \exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}\right)$
93 80 89 92 sylanbrc ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in \left\{{w}\in {J}|\exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}{w}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}\right\}$
94 93 7 eleqtrrdi ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {W}$
95 nfcv ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}$
96 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{s}\in \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}$
97 nfrab1 ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}\left\{{w}\in {J}|\exists {h}\in {Q}\phantom{\rule{.4em}{0ex}}{w}=\left\{{t}\in {T}|0<{h}\left({t}\right)\right\}\right\}$
98 7 97 nfcxfr ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{W}$
99 98 nfel2 ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {W}$
100 96 99 nfan ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left({s}\in \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\wedge \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {W}\right)$
101 eleq2 ${⊢}{w}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\to \left({s}\in {w}↔{s}\in \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\right)$
102 eleq1 ${⊢}{w}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\to \left({w}\in {W}↔\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {W}\right)$
103 101 102 anbi12d ${⊢}{w}=\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\to \left(\left({s}\in {w}\wedge {w}\in {W}\right)↔\left({s}\in \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\wedge \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {W}\right)\right)$
104 95 100 103 spcegf ${⊢}\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in \mathrm{V}\to \left(\left({s}\in \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\wedge \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {W}\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({s}\in {w}\wedge {w}\in {W}\right)\right)$
105 104 imp ${⊢}\left(\left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in \mathrm{V}\wedge \left({s}\in \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\wedge \left\{{t}\in {T}|0<{g}\left({t}\right)\right\}\in {W}\right)\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({s}\in {w}\wedge {w}\in {W}\right)$
106 46 53 94 105 syl12anc ${⊢}\left(\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\wedge \left({g}\in {Q}\wedge 0<{g}\left({s}\right)\right)\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({s}\in {w}\wedge {w}\in {W}\right)$
107 43 106 exlimddv ${⊢}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({s}\in {w}\wedge {w}\in {W}\right)$
108 nfcv ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}{s}$
109 108 98 elunif ${⊢}{s}\in \bigcup {W}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({s}\in {w}\wedge {w}\in {W}\right)$
110 107 109 sylibr ${⊢}\left({\phi }\wedge {s}\in \left({T}\setminus {U}\right)\right)\to {s}\in \bigcup {W}$
111 110 ex ${⊢}{\phi }\to \left({s}\in \left({T}\setminus {U}\right)\to {s}\in \bigcup {W}\right)$
112 111 ssrdv ${⊢}{\phi }\to {T}\setminus {U}\subseteq \bigcup {W}$