Metamath Proof Explorer


Theorem kur14lem6

Description: Lemma for kur14 . If k is the complementation operator and k is the closure operator, this expresses the identity k c k A = k c k c k c k A for any subset A of the topological space. This is the key result that lets us cut down long enough sequences of c k c k ... that arise when applying closure and complement repeatedly to A , and explains why we end up with a number as large as 1 4 , yet no larger. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses kur14lem.j J Top
kur14lem.x X = J
kur14lem.k K = cls J
kur14lem.i I = int J
kur14lem.a A X
kur14lem.b B = X K A
Assertion kur14lem6 K I K B = K B

Proof

Step Hyp Ref Expression
1 kur14lem.j J Top
2 kur14lem.x X = J
3 kur14lem.k K = cls J
4 kur14lem.i I = int J
5 kur14lem.a A X
6 kur14lem.b B = X K A
7 difss X K A X
8 6 7 eqsstri B X
9 1 2 3 4 8 kur14lem3 K B X
10 4 fveq1i I K B = int J K B
11 2 ntrss2 J Top K B X int J K B K B
12 1 9 11 mp2an int J K B K B
13 10 12 eqsstri I K B K B
14 2 clsss J Top K B X I K B K B cls J I K B cls J K B
15 1 9 13 14 mp3an cls J I K B cls J K B
16 3 fveq1i K I K B = cls J I K B
17 3 fveq1i K K B = cls J K B
18 15 16 17 3sstr4i K I K B K K B
19 1 2 3 4 8 kur14lem5 K K B = K B
20 18 19 sseqtri K I K B K B
21 1 2 3 4 9 kur14lem2 I K B = X K X K B
22 difss X K X K B X
23 21 22 eqsstri I K B X
24 1 2 3 4 5 kur14lem3 K A X
25 6 fveq2i K B = K X K A
26 25 difeq2i X K B = X K X K A
27 1 2 3 4 24 kur14lem2 I K A = X K X K A
28 4 fveq1i I K A = int J K A
29 26 27 28 3eqtr2i X K B = int J K A
30 2 ntrss2 J Top K A X int J K A K A
31 1 24 30 mp2an int J K A K A
32 29 31 eqsstri X K B K A
33 2 clsss J Top K A X X K B K A cls J X K B cls J K A
34 1 24 32 33 mp3an cls J X K B cls J K A
35 3 fveq1i K X K B = cls J X K B
36 1 2 3 4 5 kur14lem5 K K A = K A
37 3 fveq1i K K A = cls J K A
38 36 37 eqtr3i K A = cls J K A
39 34 35 38 3sstr4i K X K B K A
40 sscon K X K B K A X K A X K X K B
41 39 40 ax-mp X K A X K X K B
42 41 6 21 3sstr4i B I K B
43 2 clsss J Top I K B X B I K B cls J B cls J I K B
44 1 23 42 43 mp3an cls J B cls J I K B
45 3 fveq1i K B = cls J B
46 44 45 16 3sstr4i K B K I K B
47 20 46 eqssi K I K B = K B