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 x X y K 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 x X y K y x
4 eleq1 A = if A X A A x if A X A x
5 4 anbi1d A = if A X A A x y x X y K y x if A X A x y x X y K y x
6 5 rabbidv A = if A X A x 𝒫 𝒫 X | A x y x X y K y x = x 𝒫 𝒫 X | if A X A x y x X y K y x
7 6 inteqd A = if A X A x 𝒫 𝒫 X | A x y x X y K y x = x 𝒫 𝒫 X | if A X A x y x X y K y x
8 3 7 syl5eq A = if A X A S = x 𝒫 𝒫 X | if A X A x y x X y K y x
9 8 eleq1d A = if A X A S Fin x 𝒫 𝒫 X | if A X A x y x X y K y x Fin
10 8 fveq2d A = if A X A S = x 𝒫 𝒫 X | if A X A x y x X y K y x
11 10 breq1d A = if A X A S 14 x 𝒫 𝒫 X | if A X A x y x X y K y x 14
12 9 11 anbi12d A = if A X A S Fin S 14 x 𝒫 𝒫 X | if A X A x y x X y K y x Fin x 𝒫 𝒫 X | if A X A x y x X y K y x 14
13 unieq J = if J Top J J = if J Top J
14 1 13 syl5eq J = if J Top J X = if J Top J
15 14 pweqd J = if J Top J 𝒫 X = 𝒫 if J Top J
16 15 pweqd J = if J Top J 𝒫 𝒫 X = 𝒫 𝒫 if J Top J
17 14 sseq2d J = if J Top J A X A if J Top J
18 sn0top Top
19 18 elimel if J Top J Top
20 uniexg if J Top J Top if J Top J V
21 19 20 ax-mp if J Top J V
22 21 elpw2 A 𝒫 if J Top J A if J Top J
23 17 22 bitr4di J = if J Top J A X A 𝒫 if J Top J
24 23 ifbid J = if J Top J if A X A = if A 𝒫 if J Top J A
25 24 eleq1d J = if J Top J if A X A x if A 𝒫 if J Top J A x
26 14 difeq1d J = if J Top J X y = if J Top J y
27 fveq2 J = if J Top J cls J = cls if J Top J
28 2 27 syl5eq J = if J Top J K = cls if J Top J
29 28 fveq1d J = if J Top J K y = cls if J Top J y
30 26 29 preq12d J = if J Top J X y K y = if J Top J y cls if J Top J y
31 30 sseq1d J = if J Top J X y K y x if J Top J y cls if J Top J y x
32 31 ralbidv J = if J Top J y x X y K y x y x if J Top J y cls if J Top J y x
33 25 32 anbi12d J = if J Top J if A X A x y x X y K y x if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x
34 16 33 rabeqbidv J = if J Top J x 𝒫 𝒫 X | if A X A x y x X y K y x = x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x
35 34 inteqd J = if J Top J x 𝒫 𝒫 X | if A X A x y x X y K y x = x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x
36 35 eleq1d J = if J Top J x 𝒫 𝒫 X | if A X A x y x X y K y x Fin x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x Fin
37 35 fveq2d J = if J Top J x 𝒫 𝒫 X | if A X A x y x X y K y x = x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x
38 37 breq1d J = if J Top J x 𝒫 𝒫 X | if A X A x y x X y K y x 14 x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x 14
39 36 38 anbi12d J = if J Top J x 𝒫 𝒫 X | if A X A x y x X y K y x Fin x 𝒫 𝒫 X | if A X A x y x X y K y x 14 x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x Fin x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x 14
40 eqid if J Top J = if J Top J
41 eqid cls if J Top J = cls if J Top J
42 eqid x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x = x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x
43 0elpw 𝒫 if J Top J
44 43 elimel if A 𝒫 if J Top J A 𝒫 if J Top J
45 elpwi if A 𝒫 if J Top J A 𝒫 if J Top J if A 𝒫 if J Top J A if J Top J
46 44 45 ax-mp if A 𝒫 if J Top J A if J Top J
47 19 40 41 42 46 kur14lem10 x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J y x Fin x 𝒫 𝒫 if J Top J | if A 𝒫 if J Top J A x y x if J Top J y cls if J Top J 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