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 ⊢ 𝐽 ∈ Top
kur14lem.x ⊢ 𝑋 = ∪ 𝐽
kur14lem.k ⊢ 𝐾 = ( cls ‘ 𝐽 )
kur14lem.i ⊢ 𝐼 = ( int ‘ 𝐽 )
kur14lem.a ⊢ 𝐴 ⊆ 𝑋
kur14lem.b ⊢ 𝐵 = ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) )
Assertion kur14lem6 ( 𝐾 ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ) = ( 𝐾 ‘ 𝐵 )

Proof

Step Hyp Ref Expression
1 kur14lem.j ⊢ 𝐽 ∈ Top
2 kur14lem.x ⊢ 𝑋 = ∪ 𝐽
3 kur14lem.k ⊢ 𝐾 = ( cls ‘ 𝐽 )
4 kur14lem.i ⊢ 𝐼 = ( int ‘ 𝐽 )
5 kur14lem.a ⊢ 𝐴 ⊆ 𝑋
6 kur14lem.b ⊢ 𝐵 = ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) )
7 difss ⊢ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) ⊆ 𝑋
8 6 7 eqsstri ⊢ 𝐵 ⊆ 𝑋
9 1 2 3 4 8 kur14lem3 ⊢ ( 𝐾 ‘ 𝐵 ) ⊆ 𝑋
10 4 fveq1i ⊢ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐵 ) )
11 2 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐾 ‘ 𝐵 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐵 ) ) ⊆ ( 𝐾 ‘ 𝐵 ) )
12 1 9 11 mp2an ⊢ ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐵 ) ) ⊆ ( 𝐾 ‘ 𝐵 )
13 10 12 eqsstri ⊢ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ⊆ ( 𝐾 ‘ 𝐵 )
14 2 clsss ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐾 ‘ 𝐵 ) ⊆ 𝑋 ∧ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ⊆ ( 𝐾 ‘ 𝐵 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐵 ) ) )
15 1 9 13 14 mp3an ⊢ ( ( cls ‘ 𝐽 ) ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐵 ) )
16 3 fveq1i ⊢ ( 𝐾 ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) )
17 3 fveq1i ⊢ ( 𝐾 ‘ ( 𝐾 ‘ 𝐵 ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐵 ) )
18 15 16 17 3sstr4i ⊢ ( 𝐾 ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ) ⊆ ( 𝐾 ‘ ( 𝐾 ‘ 𝐵 ) )
19 1 2 3 4 8 kur14lem5 ⊢ ( 𝐾 ‘ ( 𝐾 ‘ 𝐵 ) ) = ( 𝐾 ‘ 𝐵 )
20 18 19 sseqtri ⊢ ( 𝐾 ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ) ⊆ ( 𝐾 ‘ 𝐵 )
21 1 2 3 4 9 kur14lem2 ⊢ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) = ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ) )
22 difss ⊢ ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ) ) ⊆ 𝑋
23 21 22 eqsstri ⊢ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ⊆ 𝑋
24 1 2 3 4 5 kur14lem3 ⊢ ( 𝐾 ‘ 𝐴 ) ⊆ 𝑋
25 6 fveq2i ⊢ ( 𝐾 ‘ 𝐵 ) = ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) )
26 25 difeq2i ⊢ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) = ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) ) )
27 1 2 3 4 24 kur14lem2 ⊢ ( 𝐼 ‘ ( 𝐾 ‘ 𝐴 ) ) = ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) ) )
28 4 fveq1i ⊢ ( 𝐼 ‘ ( 𝐾 ‘ 𝐴 ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) )
29 26 27 28 3eqtr2i ⊢ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) )
30 2 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐾 ‘ 𝐴 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) ) ⊆ ( 𝐾 ‘ 𝐴 ) )
31 1 24 30 mp2an ⊢ ( ( int ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) ) ⊆ ( 𝐾 ‘ 𝐴 )
32 29 31 eqsstri ⊢ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ⊆ ( 𝐾 ‘ 𝐴 )
33 2 clsss ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐾 ‘ 𝐴 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ⊆ ( 𝐾 ‘ 𝐴 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) ) )
34 1 24 32 33 mp3an ⊢ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) )
35 3 fveq1i ⊢ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) )
36 1 2 3 4 5 kur14lem5 ⊢ ( 𝐾 ‘ ( 𝐾 ‘ 𝐴 ) ) = ( 𝐾 ‘ 𝐴 )
37 3 fveq1i ⊢ ( 𝐾 ‘ ( 𝐾 ‘ 𝐴 ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) )
38 36 37 eqtr3i ⊢ ( 𝐾 ‘ 𝐴 ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐾 ‘ 𝐴 ) )
39 34 35 38 3sstr4i ⊢ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ) ⊆ ( 𝐾 ‘ 𝐴 )
40 sscon ⊢ ( ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ) ⊆ ( 𝐾 ‘ 𝐴 ) → ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) ⊆ ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ) ) )
41 39 40 ax-mp ⊢ ( 𝑋 ∖ ( 𝐾 ‘ 𝐴 ) ) ⊆ ( 𝑋 ∖ ( 𝐾 ‘ ( 𝑋 ∖ ( 𝐾 ‘ 𝐵 ) ) ) )
42 41 6 21 3sstr4i ⊢ 𝐵 ⊆ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) )
43 2 clsss ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ⊆ 𝑋 ∧ 𝐵 ⊆ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ) )
44 1 23 42 43 mp3an ⊢ ( ( cls ‘ 𝐽 ) ‘ 𝐵 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) )
45 3 fveq1i ⊢ ( 𝐾 ‘ 𝐵 ) = ( ( cls ‘ 𝐽 ) ‘ 𝐵 )
46 44 45 16 3sstr4i ⊢ ( 𝐾 ‘ 𝐵 ) ⊆ ( 𝐾 ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) )
47 20 46 eqssi ⊢ ( 𝐾 ‘ ( 𝐼 ‘ ( 𝐾 ‘ 𝐵 ) ) ) = ( 𝐾 ‘ 𝐵 )