# Metamath Proof Explorer

## Theorem kur14

Description: Kuratowski's closure-complement theorem. There are at most 14 sets which can be obtained by the application of the closure and complement operations to a set in a topological space. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses kur14.x ${⊢}{X}=\bigcup {J}$
kur14.k ${⊢}{K}=\mathrm{cls}\left({J}\right)$
kur14.s ${⊢}{S}=\bigcap \left\{{x}\in 𝒫𝒫{X}|\left({A}\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}$
Assertion kur14 ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\subseteq {X}\right)\to \left({S}\in \mathrm{Fin}\wedge \left|{S}\right|\le 14\right)$

### Proof

Step Hyp Ref Expression
1 kur14.x ${⊢}{X}=\bigcup {J}$
2 kur14.k ${⊢}{K}=\mathrm{cls}\left({J}\right)$
3 kur14.s ${⊢}{S}=\bigcap \left\{{x}\in 𝒫𝒫{X}|\left({A}\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}$
4 eleq1 ${⊢}{A}=if\left({A}\subseteq {X},{A},\varnothing \right)\to \left({A}\in {x}↔if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\right)$
5 4 anbi1d ${⊢}{A}=if\left({A}\subseteq {X},{A},\varnothing \right)\to \left(\left({A}\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)↔\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right)$
6 5 rabbidv ${⊢}{A}=if\left({A}\subseteq {X},{A},\varnothing \right)\to \left\{{x}\in 𝒫𝒫{X}|\left({A}\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}=\left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}$
7 6 inteqd ${⊢}{A}=if\left({A}\subseteq {X},{A},\varnothing \right)\to \bigcap \left\{{x}\in 𝒫𝒫{X}|\left({A}\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}=\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}$
8 3 7 syl5eq ${⊢}{A}=if\left({A}\subseteq {X},{A},\varnothing \right)\to {S}=\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}$
9 8 eleq1d ${⊢}{A}=if\left({A}\subseteq {X},{A},\varnothing \right)\to \left({S}\in \mathrm{Fin}↔\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\in \mathrm{Fin}\right)$
10 8 fveq2d ${⊢}{A}=if\left({A}\subseteq {X},{A},\varnothing \right)\to \left|{S}\right|=\left|\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|$
11 10 breq1d ${⊢}{A}=if\left({A}\subseteq {X},{A},\varnothing \right)\to \left(\left|{S}\right|\le 14↔\left|\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|\le 14\right)$
12 9 11 anbi12d ${⊢}{A}=if\left({A}\subseteq {X},{A},\varnothing \right)\to \left(\left({S}\in \mathrm{Fin}\wedge \left|{S}\right|\le 14\right)↔\left(\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\in \mathrm{Fin}\wedge \left|\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|\le 14\right)\right)$
13 unieq ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \bigcup {J}=\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
14 1 13 syl5eq ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to {X}=\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
15 14 pweqd ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to 𝒫{X}=𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
16 15 pweqd ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to 𝒫𝒫{X}=𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
17 14 sseq2d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left({A}\subseteq {X}↔{A}\subseteq \bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)$
18 sn0top ${⊢}\left\{\varnothing \right\}\in \mathrm{Top}$
19 18 elimel ${⊢}if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\in \mathrm{Top}$
20 uniexg ${⊢}if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\in \mathrm{Top}\to \bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\in \mathrm{V}$
21 19 20 ax-mp ${⊢}\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\in \mathrm{V}$
22 21 elpw2 ${⊢}{A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)↔{A}\subseteq \bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
23 17 22 syl6bbr ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left({A}\subseteq {X}↔{A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)$
24 23 ifbid ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to if\left({A}\subseteq {X},{A},\varnothing \right)=if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)$
25 24 eleq1d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}↔if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\right)$
26 14 difeq1d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to {X}\setminus {y}=\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y}$
27 fveq2 ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \mathrm{cls}\left({J}\right)=\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)$
28 2 27 syl5eq ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to {K}=\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)$
29 28 fveq1d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to {K}\left({y}\right)=\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)$
30 26 29 preq12d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left\{{X}\setminus {y},{K}\left({y}\right)\right\}=\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}$
31 30 sseq1d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left(\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}↔\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)$
32 31 ralbidv ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}↔\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)$
33 25 32 anbi12d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left(\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)↔\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right)$
34 16 33 rabeqbidv ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}=\left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}$
35 34 inteqd ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}=\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}$
36 35 eleq1d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left(\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\in \mathrm{Fin}↔\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}\in \mathrm{Fin}\right)$
37 35 fveq2d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left|\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|=\left|\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|$
38 37 breq1d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left(\left|\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|\le 14↔\left|\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|\le 14\right)$
39 36 38 anbi12d ${⊢}{J}=if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to \left(\left(\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\in \mathrm{Fin}\wedge \left|\bigcap \left\{{x}\in 𝒫𝒫{X}|\left(if\left({A}\subseteq {X},{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{{X}\setminus {y},{K}\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|\le 14\right)↔\left(\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}\in \mathrm{Fin}\wedge \left|\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|\le 14\right)\right)$
40 eqid ${⊢}\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)=\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
41 eqid ${⊢}\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)=\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)$
42 eqid ${⊢}\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}=\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}$
43 0elpw ${⊢}\varnothing \in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
44 43 elimel ${⊢}if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
45 elpwi ${⊢}if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\to if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\subseteq \bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
46 44 45 ax-mp ${⊢}if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\subseteq \bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)$
47 19 40 41 42 46 kur14lem10 ${⊢}\left(\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}\in \mathrm{Fin}\wedge \left|\bigcap \left\{{x}\in 𝒫𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)|\left(if\left({A}\in 𝒫\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right),{A},\varnothing \right)\in {x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left\{\bigcup if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\setminus {y},\mathrm{cls}\left(if\left({J}\in \mathrm{Top},{J},\left\{\varnothing \right\}\right)\right)\left({y}\right)\right\}\subseteq {x}\right)\right\}\right|\le 14\right)$
48 12 39 47 dedth2h ${⊢}\left({A}\subseteq {X}\wedge {J}\in \mathrm{Top}\right)\to \left({S}\in \mathrm{Fin}\wedge \left|{S}\right|\le 14\right)$
49 48 ancoms ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\subseteq {X}\right)\to \left({S}\in \mathrm{Fin}\wedge \left|{S}\right|\le 14\right)$