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 \in Top$
	kur14lem.x	$⊢ X = ⋃ J$
	kur14lem.k	$⊢ K = cls (J)$
	kur14lem.i	$⊢ I = int (J)$
	kur14lem.a	$⊢ A \subseteq X$
	kur14lem.b	$⊢ B = X ∖ K (A)$
Assertion	kur14lem6	$⊢ K (I (K (B))) = K (B)$

Proof

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

Metamath Proof Explorer

Theorem kur14lem6

Proof