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=⋃J
kur14.k ⊢K=cls⁡J
kur14.s ⊢S=⋂x∈𝒫𝒫X|A∈x∧∀y∈xX∖yK⁡y⊆x
Assertion kur14 ⊢J∈Top∧A⊆X→S∈Fin∧S≤14

Proof

Step Hyp Ref Expression
1 kur14.x ⊢X=⋃J
2 kur14.k ⊢K=cls⁡J
3 kur14.s ⊢S=⋂x∈𝒫𝒫X|A∈x∧∀y∈xX∖yK⁡y⊆x
4 eleq1 ⊢A=ifA⊆XA∅→A∈x↔ifA⊆XA∅∈x
5 4 anbi1d ⊢A=ifA⊆XA∅→A∈x∧∀y∈xX∖yK⁡y⊆x↔ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x
6 5 rabbidv ⊢A=ifA⊆XA∅→x∈𝒫𝒫X|A∈x∧∀y∈xX∖yK⁡y⊆x=x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x
7 6 inteqd ⊢A=ifA⊆XA∅→⋂x∈𝒫𝒫X|A∈x∧∀y∈xX∖yK⁡y⊆x=⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x
8 3 7 eqtrid ⊢A=ifA⊆XA∅→S=⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x
9 8 eleq1d ⊢A=ifA⊆XA∅→S∈Fin↔⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x∈Fin
10 8 fveq2d ⊢A=ifA⊆XA∅→S=⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x
11 10 breq1d ⊢A=ifA⊆XA∅→S≤14↔⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x≤14
12 9 11 anbi12d ⊢A=ifA⊆XA∅→S∈Fin∧S≤14↔⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x∈Fin∧⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x≤14
13 unieq ⊢J=ifJ∈TopJ∅→⋃J=⋃ifJ∈TopJ∅
14 1 13 eqtrid ⊢J=ifJ∈TopJ∅→X=⋃ifJ∈TopJ∅
15 14 pweqd ⊢J=ifJ∈TopJ∅→𝒫X=𝒫⋃ifJ∈TopJ∅
16 15 pweqd ⊢J=ifJ∈TopJ∅→𝒫𝒫X=𝒫𝒫⋃ifJ∈TopJ∅
17 14 sseq2d ⊢J=ifJ∈TopJ∅→A⊆X↔A⊆⋃ifJ∈TopJ∅
18 sn0top ⊢∅∈Top
19 18 elimel ⊢ifJ∈TopJ∅∈Top
20 uniexg ⊢ifJ∈TopJ∅∈Top→⋃ifJ∈TopJ∅∈V
21 19 20 ax-mp ⊢⋃ifJ∈TopJ∅∈V
22 21 elpw2 ⊢A∈𝒫⋃ifJ∈TopJ∅↔A⊆⋃ifJ∈TopJ∅
23 17 22 bitr4di ⊢J=ifJ∈TopJ∅→A⊆X↔A∈𝒫⋃ifJ∈TopJ∅
24 23 ifbid ⊢J=ifJ∈TopJ∅→ifA⊆XA∅=ifA∈𝒫⋃ifJ∈TopJ∅A∅
25 24 eleq1d ⊢J=ifJ∈TopJ∅→ifA⊆XA∅∈x↔ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x
26 14 difeq1d ⊢J=ifJ∈TopJ∅→X∖y=⋃ifJ∈TopJ∅∖y
27 fveq2 ⊢J=ifJ∈TopJ∅→cls⁡J=cls⁡ifJ∈TopJ∅
28 2 27 eqtrid ⊢J=ifJ∈TopJ∅→K=cls⁡ifJ∈TopJ∅
29 28 fveq1d ⊢J=ifJ∈TopJ∅→K⁡y=cls⁡ifJ∈TopJ∅⁡y
30 26 29 preq12d ⊢J=ifJ∈TopJ∅→X∖yK⁡y=⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y
31 30 sseq1d ⊢J=ifJ∈TopJ∅→X∖yK⁡y⊆x↔⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x
32 31 ralbidv ⊢J=ifJ∈TopJ∅→∀y∈xX∖yK⁡y⊆x↔∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x
33 25 32 anbi12d ⊢J=ifJ∈TopJ∅→ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x↔ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x
34 16 33 rabeqbidv ⊢J=ifJ∈TopJ∅→x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x=x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x
35 34 inteqd ⊢J=ifJ∈TopJ∅→⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x=⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x
36 35 eleq1d ⊢J=ifJ∈TopJ∅→⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x∈Fin↔⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x∈Fin
37 35 fveq2d ⊢J=ifJ∈TopJ∅→⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x=⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x
38 37 breq1d ⊢J=ifJ∈TopJ∅→⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x≤14↔⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x≤14
39 36 38 anbi12d ⊢J=ifJ∈TopJ∅→⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x∈Fin∧⋂x∈𝒫𝒫X|ifA⊆XA∅∈x∧∀y∈xX∖yK⁡y⊆x≤14↔⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x∈Fin∧⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x≤14
40 eqid ⊢⋃ifJ∈TopJ∅=⋃ifJ∈TopJ∅
41 eqid ⊢cls⁡ifJ∈TopJ∅=cls⁡ifJ∈TopJ∅
42 eqid ⊢⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x=⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x
43 0elpw ⊢∅∈𝒫⋃ifJ∈TopJ∅
44 43 elimel ⊢ifA∈𝒫⋃ifJ∈TopJ∅A∅∈𝒫⋃ifJ∈TopJ∅
45 elpwi ⊢ifA∈𝒫⋃ifJ∈TopJ∅A∅∈𝒫⋃ifJ∈TopJ∅→ifA∈𝒫⋃ifJ∈TopJ∅A∅⊆⋃ifJ∈TopJ∅
46 44 45 ax-mp ⊢ifA∈𝒫⋃ifJ∈TopJ∅A∅⊆⋃ifJ∈TopJ∅
47 19 40 41 42 46 kur14lem10 ⊢⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x∈Fin∧⋂x∈𝒫𝒫⋃ifJ∈TopJ∅|ifA∈𝒫⋃ifJ∈TopJ∅A∅∈x∧∀y∈x⋃ifJ∈TopJ∅∖ycls⁡ifJ∈TopJ∅⁡y⊆x≤14
48 12 39 47 dedth2h ⊢A⊆X∧J∈Top→S∈Fin∧S≤14
49 48 ancoms ⊢J∈Top∧A⊆X→S∈Fin∧S≤14