# Metamath Proof Explorer

## Theorem lbsextlem3

Description: Lemma for lbsext . A chain in S has an upper bound in S . (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsext.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lbsext.j ${⊢}{J}=\mathrm{LBasis}\left({W}\right)$
lbsext.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lbsext.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
lbsext.c ${⊢}{\phi }\to {C}\subseteq {V}$
lbsext.x ${⊢}{\phi }\to \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({C}\setminus \left\{{x}\right\}\right)$
lbsext.s ${⊢}{S}=\left\{{z}\in 𝒫{V}|\left({C}\subseteq {z}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)\right)\right\}$
lbsext.p ${⊢}{P}=\mathrm{LSubSp}\left({W}\right)$
lbsext.a ${⊢}{\phi }\to {A}\subseteq {S}$
lbsext.z ${⊢}{\phi }\to {A}\ne \varnothing$
lbsext.r ${⊢}{\phi }\to \left[\subset \right]\mathrm{Or}{A}$
lbsext.t ${⊢}{T}=\bigcup _{{u}\in {A}}{N}\left({u}\setminus \left\{{x}\right\}\right)$
Assertion lbsextlem3 ${⊢}{\phi }\to \bigcup {A}\in {S}$

### Proof

Step Hyp Ref Expression
1 lbsext.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lbsext.j ${⊢}{J}=\mathrm{LBasis}\left({W}\right)$
3 lbsext.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
4 lbsext.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
5 lbsext.c ${⊢}{\phi }\to {C}\subseteq {V}$
6 lbsext.x ${⊢}{\phi }\to \forall {x}\in {C}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({C}\setminus \left\{{x}\right\}\right)$
7 lbsext.s ${⊢}{S}=\left\{{z}\in 𝒫{V}|\left({C}\subseteq {z}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)\right)\right\}$
8 lbsext.p ${⊢}{P}=\mathrm{LSubSp}\left({W}\right)$
9 lbsext.a ${⊢}{\phi }\to {A}\subseteq {S}$
10 lbsext.z ${⊢}{\phi }\to {A}\ne \varnothing$
11 lbsext.r ${⊢}{\phi }\to \left[\subset \right]\mathrm{Or}{A}$
12 lbsext.t ${⊢}{T}=\bigcup _{{u}\in {A}}{N}\left({u}\setminus \left\{{x}\right\}\right)$
13 7 ssrab3 ${⊢}{S}\subseteq 𝒫{V}$
14 9 13 sstrdi ${⊢}{\phi }\to {A}\subseteq 𝒫{V}$
15 sspwuni ${⊢}{A}\subseteq 𝒫{V}↔\bigcup {A}\subseteq {V}$
16 14 15 sylib ${⊢}{\phi }\to \bigcup {A}\subseteq {V}$
17 1 fvexi ${⊢}{V}\in \mathrm{V}$
18 17 elpw2 ${⊢}\bigcup {A}\in 𝒫{V}↔\bigcup {A}\subseteq {V}$
19 16 18 sylibr ${⊢}{\phi }\to \bigcup {A}\in 𝒫{V}$
20 ssintub ${⊢}{C}\subseteq \bigcap \left\{{z}\in 𝒫{V}|{C}\subseteq {z}\right\}$
21 simpl ${⊢}\left({C}\subseteq {z}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)\right)\to {C}\subseteq {z}$
22 21 a1i ${⊢}{z}\in 𝒫{V}\to \left(\left({C}\subseteq {z}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)\right)\to {C}\subseteq {z}\right)$
23 22 ss2rabi ${⊢}\left\{{z}\in 𝒫{V}|\left({C}\subseteq {z}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)\right)\right\}\subseteq \left\{{z}\in 𝒫{V}|{C}\subseteq {z}\right\}$
24 7 23 eqsstri ${⊢}{S}\subseteq \left\{{z}\in 𝒫{V}|{C}\subseteq {z}\right\}$
25 9 24 sstrdi ${⊢}{\phi }\to {A}\subseteq \left\{{z}\in 𝒫{V}|{C}\subseteq {z}\right\}$
26 intss ${⊢}{A}\subseteq \left\{{z}\in 𝒫{V}|{C}\subseteq {z}\right\}\to \bigcap \left\{{z}\in 𝒫{V}|{C}\subseteq {z}\right\}\subseteq \bigcap {A}$
27 25 26 syl ${⊢}{\phi }\to \bigcap \left\{{z}\in 𝒫{V}|{C}\subseteq {z}\right\}\subseteq \bigcap {A}$
28 20 27 sstrid ${⊢}{\phi }\to {C}\subseteq \bigcap {A}$
29 intssuni ${⊢}{A}\ne \varnothing \to \bigcap {A}\subseteq \bigcup {A}$
30 10 29 syl ${⊢}{\phi }\to \bigcap {A}\subseteq \bigcup {A}$
31 28 30 sstrd ${⊢}{\phi }\to {C}\subseteq \bigcup {A}$
32 eluni2 ${⊢}{x}\in \bigcup {A}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}$
33 simpll1 ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {\phi }$
34 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
35 4 34 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
36 33 35 syl ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {W}\in \mathrm{LMod}$
37 33 9 syl ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {A}\subseteq {S}$
38 33 11 syl ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to \left[\subset \right]\mathrm{Or}{A}$
39 simpll2 ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {y}\in {A}$
40 simplr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {u}\in {A}$
41 sorpssun ${⊢}\left(\left[\subset \right]\mathrm{Or}{A}\wedge \left({y}\in {A}\wedge {u}\in {A}\right)\right)\to {y}\cup {u}\in {A}$
42 38 39 40 41 syl12anc ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {y}\cup {u}\in {A}$
43 37 42 sseldd ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {y}\cup {u}\in {S}$
44 13 43 sseldi ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {y}\cup {u}\in 𝒫{V}$
45 44 elpwid ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {y}\cup {u}\subseteq {V}$
46 45 ssdifssd ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to \left({y}\cup {u}\right)\setminus \left\{{x}\right\}\subseteq {V}$
47 ssun2 ${⊢}{u}\subseteq {y}\cup {u}$
48 ssdif ${⊢}{u}\subseteq {y}\cup {u}\to {u}\setminus \left\{{x}\right\}\subseteq \left({y}\cup {u}\right)\setminus \left\{{x}\right\}$
49 47 48 mp1i ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {u}\setminus \left\{{x}\right\}\subseteq \left({y}\cup {u}\right)\setminus \left\{{x}\right\}$
50 1 3 lspss ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({y}\cup {u}\right)\setminus \left\{{x}\right\}\subseteq {V}\wedge {u}\setminus \left\{{x}\right\}\subseteq \left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)\to {N}\left({u}\setminus \left\{{x}\right\}\right)\subseteq {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)$
51 36 46 49 50 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {N}\left({u}\setminus \left\{{x}\right\}\right)\subseteq {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)$
52 simpr ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)$
53 51 52 sseldd ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)$
54 sseq2 ${⊢}{z}={y}\cup {u}\to \left({C}\subseteq {z}↔{C}\subseteq {y}\cup {u}\right)$
55 difeq1 ${⊢}{z}={y}\cup {u}\to {z}\setminus \left\{{x}\right\}=\left({y}\cup {u}\right)\setminus \left\{{x}\right\}$
56 55 fveq2d ${⊢}{z}={y}\cup {u}\to {N}\left({z}\setminus \left\{{x}\right\}\right)={N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)$
57 56 eleq2d ${⊢}{z}={y}\cup {u}\to \left({x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)↔{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)\right)$
58 57 notbid ${⊢}{z}={y}\cup {u}\to \left(¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)↔¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)\right)$
59 58 raleqbi1dv ${⊢}{z}={y}\cup {u}\to \left(\forall {x}\in {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)↔\forall {x}\in \left({y}\cup {u}\right)\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)\right)$
60 54 59 anbi12d ${⊢}{z}={y}\cup {u}\to \left(\left({C}\subseteq {z}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)\right)↔\left({C}\subseteq {y}\cup {u}\wedge \forall {x}\in \left({y}\cup {u}\right)\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)\right)\right)$
61 60 7 elrab2 ${⊢}{y}\cup {u}\in {S}↔\left({y}\cup {u}\in 𝒫{V}\wedge \left({C}\subseteq {y}\cup {u}\wedge \forall {x}\in \left({y}\cup {u}\right)\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)\right)\right)$
62 61 simprbi ${⊢}{y}\cup {u}\in {S}\to \left({C}\subseteq {y}\cup {u}\wedge \forall {x}\in \left({y}\cup {u}\right)\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)\right)$
63 62 simprd ${⊢}{y}\cup {u}\in {S}\to \forall {x}\in \left({y}\cup {u}\right)\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)$
64 43 63 syl ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to \forall {x}\in \left({y}\cup {u}\right)\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)$
65 simpll3 ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {x}\in {y}$
66 elun1 ${⊢}{x}\in {y}\to {x}\in \left({y}\cup {u}\right)$
67 65 66 syl ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to {x}\in \left({y}\cup {u}\right)$
68 rsp ${⊢}\forall {x}\in \left({y}\cup {u}\right)\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)\to \left({x}\in \left({y}\cup {u}\right)\to ¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)\right)$
69 64 67 68 sylc ${⊢}\left(\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\wedge {x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)\to ¬{x}\in {N}\left(\left({y}\cup {u}\right)\setminus \left\{{x}\right\}\right)$
70 53 69 pm2.65da ${⊢}\left(\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\wedge {u}\in {A}\right)\to ¬{x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)$
71 70 nrexdv ${⊢}\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\to ¬\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)$
72 1 2 3 4 5 6 7 8 9 10 11 12 lbsextlem2 ${⊢}{\phi }\to \left({T}\in {P}\wedge \bigcup {A}\setminus \left\{{x}\right\}\subseteq {T}\right)$
73 72 simpld ${⊢}{\phi }\to {T}\in {P}$
74 1 8 lssss ${⊢}{T}\in {P}\to {T}\subseteq {V}$
75 73 74 syl ${⊢}{\phi }\to {T}\subseteq {V}$
76 72 simprd ${⊢}{\phi }\to \bigcup {A}\setminus \left\{{x}\right\}\subseteq {T}$
77 1 3 lspss ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\subseteq {V}\wedge \bigcup {A}\setminus \left\{{x}\right\}\subseteq {T}\right)\to {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\subseteq {N}\left({T}\right)$
78 35 75 76 77 syl3anc ${⊢}{\phi }\to {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\subseteq {N}\left({T}\right)$
79 8 3 lspid ${⊢}\left({W}\in \mathrm{LMod}\wedge {T}\in {P}\right)\to {N}\left({T}\right)={T}$
80 35 73 79 syl2anc ${⊢}{\phi }\to {N}\left({T}\right)={T}$
81 78 80 sseqtrd ${⊢}{\phi }\to {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\subseteq {T}$
82 81 3ad2ant1 ${⊢}\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\to {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\subseteq {T}$
83 82 12 sseqtrdi ${⊢}\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\to {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\subseteq \bigcup _{{u}\in {A}}{N}\left({u}\setminus \left\{{x}\right\}\right)$
84 83 sseld ${⊢}\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\to \left({x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\to {x}\in \bigcup _{{u}\in {A}}{N}\left({u}\setminus \left\{{x}\right\}\right)\right)$
85 eliun ${⊢}{x}\in \bigcup _{{u}\in {A}}{N}\left({u}\setminus \left\{{x}\right\}\right)↔\exists {u}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)$
86 84 85 syl6ib ${⊢}\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\to \left({x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\to \exists {u}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {N}\left({u}\setminus \left\{{x}\right\}\right)\right)$
87 71 86 mtod ${⊢}\left({\phi }\wedge {y}\in {A}\wedge {x}\in {y}\right)\to ¬{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)$
88 87 rexlimdv3a ${⊢}{\phi }\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to ¬{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\right)$
89 32 88 syl5bi ${⊢}{\phi }\to \left({x}\in \bigcup {A}\to ¬{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\right)$
90 89 ralrimiv ${⊢}{\phi }\to \forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)$
91 31 90 jca ${⊢}{\phi }\to \left({C}\subseteq \bigcup {A}\wedge \forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\right)$
92 sseq2 ${⊢}{z}=\bigcup {A}\to \left({C}\subseteq {z}↔{C}\subseteq \bigcup {A}\right)$
93 difeq1 ${⊢}{z}=\bigcup {A}\to {z}\setminus \left\{{x}\right\}=\bigcup {A}\setminus \left\{{x}\right\}$
94 93 fveq2d ${⊢}{z}=\bigcup {A}\to {N}\left({z}\setminus \left\{{x}\right\}\right)={N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)$
95 94 eleq2d ${⊢}{z}=\bigcup {A}\to \left({x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)↔{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\right)$
96 95 notbid ${⊢}{z}=\bigcup {A}\to \left(¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)↔¬{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\right)$
97 96 raleqbi1dv ${⊢}{z}=\bigcup {A}\to \left(\forall {x}\in {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)↔\forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\right)$
98 92 97 anbi12d ${⊢}{z}=\bigcup {A}\to \left(\left({C}\subseteq {z}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left({z}\setminus \left\{{x}\right\}\right)\right)↔\left({C}\subseteq \bigcup {A}\wedge \forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\right)\right)$
99 98 7 elrab2 ${⊢}\bigcup {A}\in {S}↔\left(\bigcup {A}\in 𝒫{V}\wedge \left({C}\subseteq \bigcup {A}\wedge \forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {N}\left(\bigcup {A}\setminus \left\{{x}\right\}\right)\right)\right)$
100 19 91 99 sylanbrc ${⊢}{\phi }\to \bigcup {A}\in {S}$