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 e. Top
kur14lem.x 
|- X = U. J
kur14lem.k 
|- K = ( cls ` J )
kur14lem.i 
|- I = ( int ` J )
kur14lem.a 
|- A C_ X
kur14lem.b 
|- B = ( X \ ( K ` A ) )
Assertion kur14lem6 
|- ( K ` ( I ` ( K ` B ) ) ) = ( K ` B )

Proof

Step Hyp Ref Expression
1 kur14lem.j 
 |-  J e. Top
2 kur14lem.x 
 |-  X = U. J
3 kur14lem.k 
 |-  K = ( cls ` J )
4 kur14lem.i 
 |-  I = ( int ` J )
5 kur14lem.a 
 |-  A C_ X
6 kur14lem.b 
 |-  B = ( X \ ( K ` A ) )
7 difss 
 |-  ( X \ ( K ` A ) ) C_ X
8 6 7 eqsstri 
 |-  B C_ X
9 1 2 3 4 8 kur14lem3 
 |-  ( K ` B ) C_ X
10 4 fveq1i 
 |-  ( I ` ( K ` B ) ) = ( ( int ` J ) ` ( K ` B ) )
11 2 ntrss2 
 |-  ( ( J e. Top /\ ( K ` B ) C_ X ) -> ( ( int ` J ) ` ( K ` B ) ) C_ ( K ` B ) )
12 1 9 11 mp2an 
 |-  ( ( int ` J ) ` ( K ` B ) ) C_ ( K ` B )
13 10 12 eqsstri 
 |-  ( I ` ( K ` B ) ) C_ ( K ` B )
14 2 clsss 
 |-  ( ( J e. Top /\ ( K ` B ) C_ X /\ ( I ` ( K ` B ) ) C_ ( K ` B ) ) -> ( ( cls ` J ) ` ( I ` ( K ` B ) ) ) C_ ( ( cls ` J ) ` ( K ` B ) ) )
15 1 9 13 14 mp3an 
 |-  ( ( cls ` J ) ` ( I ` ( K ` B ) ) ) C_ ( ( 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 ) ) ) C_ ( K ` ( K ` B ) )
19 1 2 3 4 8 kur14lem5 
 |-  ( K ` ( K ` B ) ) = ( K ` B )
20 18 19 sseqtri 
 |-  ( K ` ( I ` ( K ` B ) ) ) C_ ( K ` B )
21 1 2 3 4 9 kur14lem2 
 |-  ( I ` ( K ` B ) ) = ( X \ ( K ` ( X \ ( K ` B ) ) ) )
22 difss 
 |-  ( X \ ( K ` ( X \ ( K ` B ) ) ) ) C_ X
23 21 22 eqsstri 
 |-  ( I ` ( K ` B ) ) C_ X
24 1 2 3 4 5 kur14lem3 
 |-  ( K ` A ) C_ 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 e. Top /\ ( K ` A ) C_ X ) -> ( ( int ` J ) ` ( K ` A ) ) C_ ( K ` A ) )
31 1 24 30 mp2an 
 |-  ( ( int ` J ) ` ( K ` A ) ) C_ ( K ` A )
32 29 31 eqsstri 
 |-  ( X \ ( K ` B ) ) C_ ( K ` A )
33 2 clsss 
 |-  ( ( J e. Top /\ ( K ` A ) C_ X /\ ( X \ ( K ` B ) ) C_ ( K ` A ) ) -> ( ( cls ` J ) ` ( X \ ( K ` B ) ) ) C_ ( ( cls ` J ) ` ( K ` A ) ) )
34 1 24 32 33 mp3an 
 |-  ( ( cls ` J ) ` ( X \ ( K ` B ) ) ) C_ ( ( 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 ) ) ) C_ ( K ` A )
40 sscon 
 |-  ( ( K ` ( X \ ( K ` B ) ) ) C_ ( K ` A ) -> ( X \ ( K ` A ) ) C_ ( X \ ( K ` ( X \ ( K ` B ) ) ) ) )
41 39 40 ax-mp 
 |-  ( X \ ( K ` A ) ) C_ ( X \ ( K ` ( X \ ( K ` B ) ) ) )
42 41 6 21 3sstr4i 
 |-  B C_ ( I ` ( K ` B ) )
43 2 clsss 
 |-  ( ( J e. Top /\ ( I ` ( K ` B ) ) C_ X /\ B C_ ( I ` ( K ` B ) ) ) -> ( ( cls ` J ) ` B ) C_ ( ( cls ` J ) ` ( I ` ( K ` B ) ) ) )
44 1 23 42 43 mp3an 
 |-  ( ( cls ` J ) ` B ) C_ ( ( cls ` J ) ` ( I ` ( K ` B ) ) )
45 3 fveq1i 
 |-  ( K ` B ) = ( ( cls ` J ) ` B )
46 44 45 16 3sstr4i 
 |-  ( K ` B ) C_ ( K ` ( I ` ( K ` B ) ) )
47 20 46 eqssi 
 |-  ( K ` ( I ` ( K ` B ) ) ) = ( K ` B )