Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  kur14lem6 Structured version   Visualization version   GIF version

Theorem kur14lem6 32355
Description: Lemma for kur14 32360. If 𝑘 is the complementation operator and 𝑘 is the closure operator, this expresses the identity 𝑘𝑐𝑘𝐴 = 𝑘𝑐𝑘𝑐𝑘𝑐𝑘𝐴 for any subset 𝐴 of the topological space. This is the key result that lets us cut down long enough sequences of 𝑐𝑘𝑐𝑘... that arise when applying closure and complement repeatedly to 𝐴, and explains why we end up with a number as large as 14, yet no larger. (Contributed by Mario Carneiro, 11-Feb-2015.)
Hypotheses
Ref Expression
kur14lem.j 𝐽 ∈ Top
kur14lem.x 𝑋 = 𝐽
kur14lem.k 𝐾 = (cls‘𝐽)
kur14lem.i 𝐼 = (int‘𝐽)
kur14lem.a 𝐴𝑋
kur14lem.b 𝐵 = (𝑋 ∖ (𝐾𝐴))
Assertion
Ref Expression
kur14lem6 (𝐾‘(𝐼‘(𝐾𝐵))) = (𝐾𝐵)

Proof of Theorem kur14lem6
StepHypRef Expression
1 kur14lem.j . . . . 5 𝐽 ∈ Top
2 kur14lem.x . . . . . 6 𝑋 = 𝐽
3 kur14lem.k . . . . . 6 𝐾 = (cls‘𝐽)
4 kur14lem.i . . . . . 6 𝐼 = (int‘𝐽)
5 kur14lem.b . . . . . . 7 𝐵 = (𝑋 ∖ (𝐾𝐴))
6 difss 4105 . . . . . . 7 (𝑋 ∖ (𝐾𝐴)) ⊆ 𝑋
75, 6eqsstri 3998 . . . . . 6 𝐵𝑋
81, 2, 3, 4, 7kur14lem3 32352 . . . . 5 (𝐾𝐵) ⊆ 𝑋
94fveq1i 6664 . . . . . 6 (𝐼‘(𝐾𝐵)) = ((int‘𝐽)‘(𝐾𝐵))
102ntrss2 21593 . . . . . . 7 ((𝐽 ∈ Top ∧ (𝐾𝐵) ⊆ 𝑋) → ((int‘𝐽)‘(𝐾𝐵)) ⊆ (𝐾𝐵))
111, 8, 10mp2an 688 . . . . . 6 ((int‘𝐽)‘(𝐾𝐵)) ⊆ (𝐾𝐵)
129, 11eqsstri 3998 . . . . 5 (𝐼‘(𝐾𝐵)) ⊆ (𝐾𝐵)
132clsss 21590 . . . . 5 ((𝐽 ∈ Top ∧ (𝐾𝐵) ⊆ 𝑋 ∧ (𝐼‘(𝐾𝐵)) ⊆ (𝐾𝐵)) → ((cls‘𝐽)‘(𝐼‘(𝐾𝐵))) ⊆ ((cls‘𝐽)‘(𝐾𝐵)))
141, 8, 12, 13mp3an 1452 . . . 4 ((cls‘𝐽)‘(𝐼‘(𝐾𝐵))) ⊆ ((cls‘𝐽)‘(𝐾𝐵))
153fveq1i 6664 . . . 4 (𝐾‘(𝐼‘(𝐾𝐵))) = ((cls‘𝐽)‘(𝐼‘(𝐾𝐵)))
163fveq1i 6664 . . . 4 (𝐾‘(𝐾𝐵)) = ((cls‘𝐽)‘(𝐾𝐵))
1714, 15, 163sstr4i 4007 . . 3 (𝐾‘(𝐼‘(𝐾𝐵))) ⊆ (𝐾‘(𝐾𝐵))
181, 2, 3, 4, 7kur14lem5 32354 . . 3 (𝐾‘(𝐾𝐵)) = (𝐾𝐵)
1917, 18sseqtri 4000 . 2 (𝐾‘(𝐼‘(𝐾𝐵))) ⊆ (𝐾𝐵)
201, 2, 3, 4, 8kur14lem2 32351 . . . . 5 (𝐼‘(𝐾𝐵)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵))))
21 difss 4105 . . . . 5 (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵)))) ⊆ 𝑋
2220, 21eqsstri 3998 . . . 4 (𝐼‘(𝐾𝐵)) ⊆ 𝑋
23 kur14lem.a . . . . . . . . 9 𝐴𝑋
241, 2, 3, 4, 23kur14lem3 32352 . . . . . . . 8 (𝐾𝐴) ⊆ 𝑋
255fveq2i 6666 . . . . . . . . . . 11 (𝐾𝐵) = (𝐾‘(𝑋 ∖ (𝐾𝐴)))
2625difeq2i 4093 . . . . . . . . . 10 (𝑋 ∖ (𝐾𝐵)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴))))
271, 2, 3, 4, 24kur14lem2 32351 . . . . . . . . . 10 (𝐼‘(𝐾𝐴)) = (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐴))))
284fveq1i 6664 . . . . . . . . . 10 (𝐼‘(𝐾𝐴)) = ((int‘𝐽)‘(𝐾𝐴))
2926, 27, 283eqtr2i 2847 . . . . . . . . 9 (𝑋 ∖ (𝐾𝐵)) = ((int‘𝐽)‘(𝐾𝐴))
302ntrss2 21593 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (𝐾𝐴) ⊆ 𝑋) → ((int‘𝐽)‘(𝐾𝐴)) ⊆ (𝐾𝐴))
311, 24, 30mp2an 688 . . . . . . . . 9 ((int‘𝐽)‘(𝐾𝐴)) ⊆ (𝐾𝐴)
3229, 31eqsstri 3998 . . . . . . . 8 (𝑋 ∖ (𝐾𝐵)) ⊆ (𝐾𝐴)
332clsss 21590 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝐾𝐴) ⊆ 𝑋 ∧ (𝑋 ∖ (𝐾𝐵)) ⊆ (𝐾𝐴)) → ((cls‘𝐽)‘(𝑋 ∖ (𝐾𝐵))) ⊆ ((cls‘𝐽)‘(𝐾𝐴)))
341, 24, 32, 33mp3an 1452 . . . . . . 7 ((cls‘𝐽)‘(𝑋 ∖ (𝐾𝐵))) ⊆ ((cls‘𝐽)‘(𝐾𝐴))
353fveq1i 6664 . . . . . . 7 (𝐾‘(𝑋 ∖ (𝐾𝐵))) = ((cls‘𝐽)‘(𝑋 ∖ (𝐾𝐵)))
361, 2, 3, 4, 23kur14lem5 32354 . . . . . . . 8 (𝐾‘(𝐾𝐴)) = (𝐾𝐴)
373fveq1i 6664 . . . . . . . 8 (𝐾‘(𝐾𝐴)) = ((cls‘𝐽)‘(𝐾𝐴))
3836, 37eqtr3i 2843 . . . . . . 7 (𝐾𝐴) = ((cls‘𝐽)‘(𝐾𝐴))
3934, 35, 383sstr4i 4007 . . . . . 6 (𝐾‘(𝑋 ∖ (𝐾𝐵))) ⊆ (𝐾𝐴)
40 sscon 4112 . . . . . 6 ((𝐾‘(𝑋 ∖ (𝐾𝐵))) ⊆ (𝐾𝐴) → (𝑋 ∖ (𝐾𝐴)) ⊆ (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵)))))
4139, 40ax-mp 5 . . . . 5 (𝑋 ∖ (𝐾𝐴)) ⊆ (𝑋 ∖ (𝐾‘(𝑋 ∖ (𝐾𝐵))))
4241, 5, 203sstr4i 4007 . . . 4 𝐵 ⊆ (𝐼‘(𝐾𝐵))
432clsss 21590 . . . 4 ((𝐽 ∈ Top ∧ (𝐼‘(𝐾𝐵)) ⊆ 𝑋𝐵 ⊆ (𝐼‘(𝐾𝐵))) → ((cls‘𝐽)‘𝐵) ⊆ ((cls‘𝐽)‘(𝐼‘(𝐾𝐵))))
441, 22, 42, 43mp3an 1452 . . 3 ((cls‘𝐽)‘𝐵) ⊆ ((cls‘𝐽)‘(𝐼‘(𝐾𝐵)))
453fveq1i 6664 . . 3 (𝐾𝐵) = ((cls‘𝐽)‘𝐵)
4644, 45, 153sstr4i 4007 . 2 (𝐾𝐵) ⊆ (𝐾‘(𝐼‘(𝐾𝐵)))
4719, 46eqssi 3980 1 (𝐾‘(𝐼‘(𝐾𝐵))) = (𝐾𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  cdif 3930  wss 3933   cuni 4830  cfv 6348  Topctop 21429  intcnt 21553  clsccl 21554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-top 21430  df-cld 21555  df-ntr 21556  df-cls 21557
This theorem is referenced by:  kur14lem7  32356
  Copyright terms: Public domain W3C validator