# Metamath Proof Explorer

## Theorem cmpsub

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman'sBeginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis cmpsub.1 ${⊢}{X}=\bigcup {J}$
Assertion cmpsub ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({J}{↾}_{𝑡}{S}\in \mathrm{Comp}↔\forall {c}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {c}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)\right)$

### Proof

Step Hyp Ref Expression
1 cmpsub.1 ${⊢}{X}=\bigcup {J}$
2 eqid ${⊢}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left({J}{↾}_{𝑡}{S}\right)$
3 2 iscmp ${⊢}{J}{↾}_{𝑡}{S}\in \mathrm{Comp}↔\left({J}{↾}_{𝑡}{S}\in \mathrm{Top}\wedge \forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)$
4 id ${⊢}{S}\subseteq {X}\to {S}\subseteq {X}$
5 1 topopn ${⊢}{J}\in \mathrm{Top}\to {X}\in {J}$
6 ssexg ${⊢}\left({S}\subseteq {X}\wedge {X}\in {J}\right)\to {S}\in \mathrm{V}$
7 4 5 6 syl2anr ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\in \mathrm{V}$
8 resttop ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}{S}\in \mathrm{Top}$
9 7 8 syldan ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {J}{↾}_{𝑡}{S}\in \mathrm{Top}$
10 ibar ${⊢}{J}{↾}_{𝑡}{S}\in \mathrm{Top}\to \left(\forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)↔\left({J}{↾}_{𝑡}{S}\in \mathrm{Top}\wedge \forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)\right)$
11 10 bicomd ${⊢}{J}{↾}_{𝑡}{S}\in \mathrm{Top}\to \left(\left({J}{↾}_{𝑡}{S}\in \mathrm{Top}\wedge \forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)↔\forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)$
12 9 11 syl ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\left({J}{↾}_{𝑡}{S}\in \mathrm{Top}\wedge \forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)↔\forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)$
13 3 12 syl5bb ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({J}{↾}_{𝑡}{S}\in \mathrm{Comp}↔\forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)$
14 vex ${⊢}{t}\in \mathrm{V}$
15 eqeq1 ${⊢}{x}={t}\to \left({x}={y}\cap {S}↔{t}={y}\cap {S}\right)$
16 15 rexbidv ${⊢}{x}={t}\to \left(\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}↔\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{t}={y}\cap {S}\right)$
17 14 16 elab ${⊢}{t}\in \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}↔\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{t}={y}\cap {S}$
18 velpw ${⊢}{c}\in 𝒫{J}↔{c}\subseteq {J}$
19 ssel2 ${⊢}\left({c}\subseteq {J}\wedge {y}\in {c}\right)\to {y}\in {J}$
20 ineq1 ${⊢}{d}={y}\to {d}\cap {S}={y}\cap {S}$
21 20 rspceeqv ${⊢}\left({y}\in {J}\wedge {t}={y}\cap {S}\right)\to \exists {d}\in {J}\phantom{\rule{.4em}{0ex}}{t}={d}\cap {S}$
22 21 ex ${⊢}{y}\in {J}\to \left({t}={y}\cap {S}\to \exists {d}\in {J}\phantom{\rule{.4em}{0ex}}{t}={d}\cap {S}\right)$
23 19 22 syl ${⊢}\left({c}\subseteq {J}\wedge {y}\in {c}\right)\to \left({t}={y}\cap {S}\to \exists {d}\in {J}\phantom{\rule{.4em}{0ex}}{t}={d}\cap {S}\right)$
24 23 ex ${⊢}{c}\subseteq {J}\to \left({y}\in {c}\to \left({t}={y}\cap {S}\to \exists {d}\in {J}\phantom{\rule{.4em}{0ex}}{t}={d}\cap {S}\right)\right)$
25 18 24 sylbi ${⊢}{c}\in 𝒫{J}\to \left({y}\in {c}\to \left({t}={y}\cap {S}\to \exists {d}\in {J}\phantom{\rule{.4em}{0ex}}{t}={d}\cap {S}\right)\right)$
26 25 adantl ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left({y}\in {c}\to \left({t}={y}\cap {S}\to \exists {d}\in {J}\phantom{\rule{.4em}{0ex}}{t}={d}\cap {S}\right)\right)$
27 26 rexlimdv ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left(\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{t}={y}\cap {S}\to \exists {d}\in {J}\phantom{\rule{.4em}{0ex}}{t}={d}\cap {S}\right)$
28 simpll ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to {J}\in \mathrm{Top}$
29 1 sseq2i ${⊢}{S}\subseteq {X}↔{S}\subseteq \bigcup {J}$
30 uniexg ${⊢}{J}\in \mathrm{Top}\to \bigcup {J}\in \mathrm{V}$
31 ssexg ${⊢}\left({S}\subseteq \bigcup {J}\wedge \bigcup {J}\in \mathrm{V}\right)\to {S}\in \mathrm{V}$
32 30 31 sylan2 ${⊢}\left({S}\subseteq \bigcup {J}\wedge {J}\in \mathrm{Top}\right)\to {S}\in \mathrm{V}$
33 32 ancoms ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq \bigcup {J}\right)\to {S}\in \mathrm{V}$
34 29 33 sylan2b ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\in \mathrm{V}$
35 34 adantr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to {S}\in \mathrm{V}$
36 elrest ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\in \mathrm{V}\right)\to \left({t}\in \left({J}{↾}_{𝑡}{S}\right)↔\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}{t}={d}\cap {S}\right)$
37 28 35 36 syl2anc ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left({t}\in \left({J}{↾}_{𝑡}{S}\right)↔\exists {d}\in {J}\phantom{\rule{.4em}{0ex}}{t}={d}\cap {S}\right)$
38 27 37 sylibrd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left(\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{t}={y}\cap {S}\to {t}\in \left({J}{↾}_{𝑡}{S}\right)\right)$
39 17 38 syl5bi ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left({t}\in \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to {t}\in \left({J}{↾}_{𝑡}{S}\right)\right)$
40 39 ssrdv ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\subseteq {J}{↾}_{𝑡}{S}$
41 vex ${⊢}{c}\in \mathrm{V}$
42 41 abrexex ${⊢}\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\in \mathrm{V}$
43 42 elpw ${⊢}\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)↔\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\subseteq {J}{↾}_{𝑡}{S}$
44 40 43 sylibr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)$
45 unieq ${⊢}{s}=\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \bigcup {s}=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}$
46 45 eqeq2d ${⊢}{s}=\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}↔\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\right)$
47 pweq ${⊢}{s}=\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to 𝒫{s}=𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}$
48 47 ineq1d ${⊢}{s}=\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to 𝒫{s}\cap \mathrm{Fin}=𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}$
49 48 rexeqdv ${⊢}{s}=\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \left(\exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}↔\exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)$
50 46 49 imbi12d ${⊢}{s}=\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \left(\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)↔\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)$
51 50 rspcva ${⊢}\left(\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\wedge \forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)\to \left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)$
52 44 51 sylan ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge \forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)\to \left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)$
53 52 ex ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left(\forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\to \left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)$
54 1 restuni ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}=\bigcup \left({J}{↾}_{𝑡}{S}\right)$
55 54 ad2antrr ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to {S}=\bigcup \left({J}{↾}_{𝑡}{S}\right)$
56 vex ${⊢}{y}\in \mathrm{V}$
57 56 inex1 ${⊢}{y}\cap {S}\in \mathrm{V}$
58 57 dfiun2 ${⊢}\bigcup _{{y}\in {c}}\left({y}\cap {S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}$
59 incom ${⊢}{y}\cap {S}={S}\cap {y}$
60 59 a1i ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge {y}\in {c}\right)\to {y}\cap {S}={S}\cap {y}$
61 60 iuneq2dv ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \bigcup _{{y}\in {c}}\left({y}\cap {S}\right)=\bigcup _{{y}\in {c}}\left({S}\cap {y}\right)$
62 58 61 syl5eqr ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}=\bigcup _{{y}\in {c}}\left({S}\cap {y}\right)$
63 iunin2 ${⊢}\bigcup _{{y}\in {c}}\left({S}\cap {y}\right)={S}\cap \bigcup _{{y}\in {c}}{y}$
64 uniiun ${⊢}\bigcup {c}=\bigcup _{{y}\in {c}}{y}$
65 64 eqcomi ${⊢}\bigcup _{{y}\in {c}}{y}=\bigcup {c}$
66 65 a1i ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \bigcup _{{y}\in {c}}{y}=\bigcup {c}$
67 66 ineq2d ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to {S}\cap \bigcup _{{y}\in {c}}{y}={S}\cap \bigcup {c}$
68 incom ${⊢}{S}\cap \bigcup {c}=\bigcup {c}\cap {S}$
69 sseqin2 ${⊢}{S}\subseteq \bigcup {c}↔\bigcup {c}\cap {S}={S}$
70 69 biimpi ${⊢}{S}\subseteq \bigcup {c}\to \bigcup {c}\cap {S}={S}$
71 68 70 syl5eq ${⊢}{S}\subseteq \bigcup {c}\to {S}\cap \bigcup {c}={S}$
72 71 adantl ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to {S}\cap \bigcup {c}={S}$
73 67 72 eqtrd ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to {S}\cap \bigcup _{{y}\in {c}}{y}={S}$
74 63 73 syl5eq ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \bigcup _{{y}\in {c}}\left({S}\cap {y}\right)={S}$
75 62 74 eqtr2d ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to {S}=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}$
76 55 75 eqeq12d ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \left({S}={S}↔\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\right)$
77 55 eqeq1d ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \left({S}=\bigcup {t}↔\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)$
78 77 rexbidv ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \left(\exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}=\bigcup {t}↔\exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)$
79 76 78 imbi12d ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \left(\left({S}={S}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}=\bigcup {t}\right)↔\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)$
80 eqid ${⊢}{S}={S}$
81 80 a1bi ${⊢}\exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}=\bigcup {t}↔\left({S}={S}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}=\bigcup {t}\right)$
82 elin ${⊢}{t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)↔\left({t}\in 𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\wedge {t}\in \mathrm{Fin}\right)$
83 velpw ${⊢}{t}\in 𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}↔{t}\subseteq \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}$
84 dfss3 ${⊢}{t}\subseteq \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}↔\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}\in \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}$
85 vex ${⊢}{s}\in \mathrm{V}$
86 eqeq1 ${⊢}{x}={s}\to \left({x}={y}\cap {S}↔{s}={y}\cap {S}\right)$
87 86 rexbidv ${⊢}{x}={s}\to \left(\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}↔\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\right)$
88 85 87 elab ${⊢}{s}\in \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}↔\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}$
89 88 ralbii ${⊢}\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}\in \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}↔\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}$
90 83 84 89 3bitri ${⊢}{t}\in 𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}↔\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}$
91 90 anbi1i ${⊢}\left({t}\in 𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\wedge {t}\in \mathrm{Fin}\right)↔\left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)$
92 82 91 bitri ${⊢}{t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)↔\left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)$
93 ineq1 ${⊢}{y}={f}\left({s}\right)\to {y}\cap {S}={f}\left({s}\right)\cap {S}$
94 93 eqeq2d ${⊢}{y}={f}\left({s}\right)\to \left({s}={y}\cap {S}↔{s}={f}\left({s}\right)\cap {S}\right)$
95 94 ac6sfi ${⊢}\left({t}\in \mathrm{Fin}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)$
96 95 ancoms ${⊢}\left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)$
97 96 adantl ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)$
98 frn ${⊢}{f}:{t}⟶{c}\to \mathrm{ran}{f}\subseteq {c}$
99 98 ad2antrl ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to \mathrm{ran}{f}\subseteq {c}$
100 vex ${⊢}{f}\in \mathrm{V}$
101 100 rnex ${⊢}\mathrm{ran}{f}\in \mathrm{V}$
102 101 elpw ${⊢}\mathrm{ran}{f}\in 𝒫{c}↔\mathrm{ran}{f}\subseteq {c}$
103 99 102 sylibr ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to \mathrm{ran}{f}\in 𝒫{c}$
104 simprr ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\to {t}\in \mathrm{Fin}$
105 104 ad2antrr ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to {t}\in \mathrm{Fin}$
106 ffn ${⊢}{f}:{t}⟶{c}\to {f}Fn{t}$
107 dffn4 ${⊢}{f}Fn{t}↔{f}:{t}\underset{onto}{⟶}\mathrm{ran}{f}$
108 106 107 sylib ${⊢}{f}:{t}⟶{c}\to {f}:{t}\underset{onto}{⟶}\mathrm{ran}{f}$
109 fodomfi ${⊢}\left({t}\in \mathrm{Fin}\wedge {f}:{t}\underset{onto}{⟶}\mathrm{ran}{f}\right)\to \mathrm{ran}{f}\preccurlyeq {t}$
110 108 109 sylan2 ${⊢}\left({t}\in \mathrm{Fin}\wedge {f}:{t}⟶{c}\right)\to \mathrm{ran}{f}\preccurlyeq {t}$
111 110 adantll ${⊢}\left(\left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\wedge {f}:{t}⟶{c}\right)\to \mathrm{ran}{f}\preccurlyeq {t}$
112 111 adantll ${⊢}\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {f}:{t}⟶{c}\right)\to \mathrm{ran}{f}\preccurlyeq {t}$
113 112 ad2ant2r ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to \mathrm{ran}{f}\preccurlyeq {t}$
114 domfi ${⊢}\left({t}\in \mathrm{Fin}\wedge \mathrm{ran}{f}\preccurlyeq {t}\right)\to \mathrm{ran}{f}\in \mathrm{Fin}$
115 105 113 114 syl2anc ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to \mathrm{ran}{f}\in \mathrm{Fin}$
116 103 115 elind ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to \mathrm{ran}{f}\in \left(𝒫{c}\cap \mathrm{Fin}\right)$
117 id ${⊢}{s}={u}\to {s}={u}$
118 fveq2 ${⊢}{s}={u}\to {f}\left({s}\right)={f}\left({u}\right)$
119 118 ineq1d ${⊢}{s}={u}\to {f}\left({s}\right)\cap {S}={f}\left({u}\right)\cap {S}$
120 117 119 eqeq12d ${⊢}{s}={u}\to \left({s}={f}\left({s}\right)\cap {S}↔{u}={f}\left({u}\right)\cap {S}\right)$
121 120 rspccv ${⊢}\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\to \left({u}\in {t}\to {u}={f}\left({u}\right)\cap {S}\right)$
122 pm2.27 ${⊢}{u}\in {t}\to \left(\left({u}\in {t}\to {u}={f}\left({u}\right)\cap {S}\right)\to {u}={f}\left({u}\right)\cap {S}\right)$
123 inss1 ${⊢}{f}\left({u}\right)\cap {S}\subseteq {f}\left({u}\right)$
124 sseq1 ${⊢}{u}={f}\left({u}\right)\cap {S}\to \left({u}\subseteq {f}\left({u}\right)↔{f}\left({u}\right)\cap {S}\subseteq {f}\left({u}\right)\right)$
125 123 124 mpbiri ${⊢}{u}={f}\left({u}\right)\cap {S}\to {u}\subseteq {f}\left({u}\right)$
126 ssel ${⊢}{u}\subseteq {f}\left({u}\right)\to \left({w}\in {u}\to {w}\in {f}\left({u}\right)\right)$
127 126 a1dd ${⊢}{u}\subseteq {f}\left({u}\right)\to \left({w}\in {u}\to \left({f}:{t}⟶{c}\to {w}\in {f}\left({u}\right)\right)\right)$
128 125 127 syl ${⊢}{u}={f}\left({u}\right)\cap {S}\to \left({w}\in {u}\to \left({f}:{t}⟶{c}\to {w}\in {f}\left({u}\right)\right)\right)$
129 128 a1i ${⊢}{u}\in {t}\to \left({u}={f}\left({u}\right)\cap {S}\to \left({w}\in {u}\to \left({f}:{t}⟶{c}\to {w}\in {f}\left({u}\right)\right)\right)\right)$
130 129 3imp ${⊢}\left({u}\in {t}\wedge {u}={f}\left({u}\right)\cap {S}\wedge {w}\in {u}\right)\to \left({f}:{t}⟶{c}\to {w}\in {f}\left({u}\right)\right)$
131 fnfvelrn ${⊢}\left({f}Fn{t}\wedge {u}\in {t}\right)\to {f}\left({u}\right)\in \mathrm{ran}{f}$
132 131 expcom ${⊢}{u}\in {t}\to \left({f}Fn{t}\to {f}\left({u}\right)\in \mathrm{ran}{f}\right)$
133 132 3ad2ant1 ${⊢}\left({u}\in {t}\wedge {u}={f}\left({u}\right)\cap {S}\wedge {w}\in {u}\right)\to \left({f}Fn{t}\to {f}\left({u}\right)\in \mathrm{ran}{f}\right)$
134 106 133 syl5 ${⊢}\left({u}\in {t}\wedge {u}={f}\left({u}\right)\cap {S}\wedge {w}\in {u}\right)\to \left({f}:{t}⟶{c}\to {f}\left({u}\right)\in \mathrm{ran}{f}\right)$
135 130 134 jcad ${⊢}\left({u}\in {t}\wedge {u}={f}\left({u}\right)\cap {S}\wedge {w}\in {u}\right)\to \left({f}:{t}⟶{c}\to \left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\right)$
136 135 3exp ${⊢}{u}\in {t}\to \left({u}={f}\left({u}\right)\cap {S}\to \left({w}\in {u}\to \left({f}:{t}⟶{c}\to \left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\right)\right)\right)$
137 122 136 syld ${⊢}{u}\in {t}\to \left(\left({u}\in {t}\to {u}={f}\left({u}\right)\cap {S}\right)\to \left({w}\in {u}\to \left({f}:{t}⟶{c}\to \left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\right)\right)\right)$
138 137 com3r ${⊢}{w}\in {u}\to \left({u}\in {t}\to \left(\left({u}\in {t}\to {u}={f}\left({u}\right)\cap {S}\right)\to \left({f}:{t}⟶{c}\to \left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\right)\right)\right)$
139 138 imp ${⊢}\left({w}\in {u}\wedge {u}\in {t}\right)\to \left(\left({u}\in {t}\to {u}={f}\left({u}\right)\cap {S}\right)\to \left({f}:{t}⟶{c}\to \left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\right)\right)$
140 139 com3l ${⊢}\left({u}\in {t}\to {u}={f}\left({u}\right)\cap {S}\right)\to \left({f}:{t}⟶{c}\to \left(\left({w}\in {u}\wedge {u}\in {t}\right)\to \left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\right)\right)$
141 140 impcom ${⊢}\left({f}:{t}⟶{c}\wedge \left({u}\in {t}\to {u}={f}\left({u}\right)\cap {S}\right)\right)\to \left(\left({w}\in {u}\wedge {u}\in {t}\right)\to \left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\right)$
142 121 141 sylan2 ${⊢}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \left(\left({w}\in {u}\wedge {u}\in {t}\right)\to \left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\right)$
143 fvex ${⊢}{f}\left({u}\right)\in \mathrm{V}$
144 eleq2 ${⊢}{v}={f}\left({u}\right)\to \left({w}\in {v}↔{w}\in {f}\left({u}\right)\right)$
145 eleq1 ${⊢}{v}={f}\left({u}\right)\to \left({v}\in \mathrm{ran}{f}↔{f}\left({u}\right)\in \mathrm{ran}{f}\right)$
146 144 145 anbi12d ${⊢}{v}={f}\left({u}\right)\to \left(\left({w}\in {v}\wedge {v}\in \mathrm{ran}{f}\right)↔\left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\right)$
147 143 146 spcev ${⊢}\left({w}\in {f}\left({u}\right)\wedge {f}\left({u}\right)\in \mathrm{ran}{f}\right)\to \exists {v}\phantom{\rule{.4em}{0ex}}\left({w}\in {v}\wedge {v}\in \mathrm{ran}{f}\right)$
148 142 147 syl6 ${⊢}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \left(\left({w}\in {u}\wedge {u}\in {t}\right)\to \exists {v}\phantom{\rule{.4em}{0ex}}\left({w}\in {v}\wedge {v}\in \mathrm{ran}{f}\right)\right)$
149 148 exlimdv ${⊢}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \left(\exists {u}\phantom{\rule{.4em}{0ex}}\left({w}\in {u}\wedge {u}\in {t}\right)\to \exists {v}\phantom{\rule{.4em}{0ex}}\left({w}\in {v}\wedge {v}\in \mathrm{ran}{f}\right)\right)$
150 eluni ${⊢}{w}\in \bigcup {t}↔\exists {u}\phantom{\rule{.4em}{0ex}}\left({w}\in {u}\wedge {u}\in {t}\right)$
151 eluni ${⊢}{w}\in \bigcup \mathrm{ran}{f}↔\exists {v}\phantom{\rule{.4em}{0ex}}\left({w}\in {v}\wedge {v}\in \mathrm{ran}{f}\right)$
152 149 150 151 3imtr4g ${⊢}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \left({w}\in \bigcup {t}\to {w}\in \bigcup \mathrm{ran}{f}\right)$
153 152 ssrdv ${⊢}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \bigcup {t}\subseteq \bigcup \mathrm{ran}{f}$
154 153 adantl ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to \bigcup {t}\subseteq \bigcup \mathrm{ran}{f}$
155 sseq1 ${⊢}{S}=\bigcup {t}\to \left({S}\subseteq \bigcup \mathrm{ran}{f}↔\bigcup {t}\subseteq \bigcup \mathrm{ran}{f}\right)$
156 155 ad2antlr ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to \left({S}\subseteq \bigcup \mathrm{ran}{f}↔\bigcup {t}\subseteq \bigcup \mathrm{ran}{f}\right)$
157 154 156 mpbird ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to {S}\subseteq \bigcup \mathrm{ran}{f}$
158 116 157 jca ${⊢}\left(\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\wedge \left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\right)\to \left(\mathrm{ran}{f}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\wedge {S}\subseteq \bigcup \mathrm{ran}{f}\right)$
159 158 ex ${⊢}\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\to \left(\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \left(\mathrm{ran}{f}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\wedge {S}\subseteq \bigcup \mathrm{ran}{f}\right)\right)$
160 159 eximdv ${⊢}\left(\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\wedge {S}=\bigcup {t}\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left(\mathrm{ran}{f}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\wedge {S}\subseteq \bigcup \mathrm{ran}{f}\right)\right)$
161 160 ex ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\to \left({S}=\bigcup {t}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left(\mathrm{ran}{f}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\wedge {S}\subseteq \bigcup \mathrm{ran}{f}\right)\right)\right)$
162 161 com23 ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \left({S}=\bigcup {t}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left(\mathrm{ran}{f}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\wedge {S}\subseteq \bigcup \mathrm{ran}{f}\right)\right)\right)$
163 unieq ${⊢}{d}=\mathrm{ran}{f}\to \bigcup {d}=\bigcup \mathrm{ran}{f}$
164 163 sseq2d ${⊢}{d}=\mathrm{ran}{f}\to \left({S}\subseteq \bigcup {d}↔{S}\subseteq \bigcup \mathrm{ran}{f}\right)$
165 164 rspcev ${⊢}\left(\mathrm{ran}{f}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\wedge {S}\subseteq \bigcup \mathrm{ran}{f}\right)\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}$
166 165 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\left(\mathrm{ran}{f}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\wedge {S}\subseteq \bigcup \mathrm{ran}{f}\right)\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}$
167 162 166 syl8 ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{t}⟶{c}\wedge \forall {s}\in {t}\phantom{\rule{.4em}{0ex}}{s}={f}\left({s}\right)\cap {S}\right)\to \left({S}=\bigcup {t}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)\right)$
168 97 167 mpd ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge \left(\forall {s}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{s}={y}\cap {S}\wedge {t}\in \mathrm{Fin}\right)\right)\to \left({S}=\bigcup {t}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)$
169 92 168 sylan2b ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\wedge {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\right)\to \left({S}=\bigcup {t}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)$
170 169 rexlimdva ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \left(\exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}=\bigcup {t}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)$
171 81 170 syl5bir ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \left(\left({S}={S}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}=\bigcup {t}\right)\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)$
172 79 171 sylbird ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\wedge {S}\subseteq \bigcup {c}\right)\to \left(\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)$
173 172 ex ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left({S}\subseteq \bigcup {c}\to \left(\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)\right)$
174 173 com23 ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left(\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup \left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\to \exists {t}\in \left(𝒫\left\{{x}|\exists {y}\in {c}\phantom{\rule{.4em}{0ex}}{x}={y}\cap {S}\right\}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\to \left({S}\subseteq \bigcup {c}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)\right)$
175 53 174 syld ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {c}\in 𝒫{J}\right)\to \left(\forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\to \left({S}\subseteq \bigcup {c}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)\right)$
176 175 ralrimdva ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\to \forall {c}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {c}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)\right)$
177 1 cmpsublem ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\forall {c}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {c}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)\to \forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)\right)$
178 176 177 impbid ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\forall {s}\in 𝒫\left({J}{↾}_{𝑡}{S}\right)\phantom{\rule{.4em}{0ex}}\left(\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {s}\to \exists {t}\in \left(𝒫{s}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup \left({J}{↾}_{𝑡}{S}\right)=\bigcup {t}\right)↔\forall {c}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {c}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)\right)$
179 13 178 bitrd ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({J}{↾}_{𝑡}{S}\in \mathrm{Comp}↔\forall {c}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq \bigcup {c}\to \exists {d}\in \left(𝒫{c}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{S}\subseteq \bigcup {d}\right)\right)$