dssmapntrcls

Description: The interior and closure operators on a topology are duals of each other. See also kur14lem2 . (Contributed by RP, 21-Apr-2021)

	Ref	Expression
Hypotheses	dssmapclsntr.x	$⊢ X = ⋃ J$
	dssmapclsntr.k	$⊢ K = cls (J)$
	dssmapclsntr.i	$⊢ I = int (J)$
	dssmapclsntr.o	$⊢ O = (b \in V ⟼ (f \in ({𝒫 b}^{𝒫 b}) ⟼ (s \in 𝒫 b ⟼ b ∖ f (b ∖ s))))$
	dssmapclsntr.d	$⊢ D = O (X)$
Assertion	dssmapntrcls	$⊢ J \in Top \to I = D (K)$

Proof

Step	Hyp	Ref	Expression
1		dssmapclsntr.x	$⊢ X = ⋃ J$
2		dssmapclsntr.k	$⊢ K = cls (J)$
3		dssmapclsntr.i	$⊢ I = int (J)$
4		dssmapclsntr.o	$⊢ O = (b \in V ⟼ (f \in ({𝒫 b}^{𝒫 b}) ⟼ (s \in 𝒫 b ⟼ b ∖ f (b ∖ s))))$
5		dssmapclsntr.d	$⊢ D = O (X)$
6		vpwex	$⊢ 𝒫 t \in V$
7	6	inex2	$⊢ J \cap 𝒫 t \in V$
8	7	uniex	$⊢ ⋃ (J \cap 𝒫 t) \in V$
9	8	rgenw	$⊢ \forall t \in 𝒫 X ⋃ (J \cap 𝒫 t) \in V$
10		nfcv	$⊢ \underline{Ⅎ} t 𝒫 X$
11	10	fnmptf	$⊢ \forall t \in 𝒫 X ⋃ (J \cap 𝒫 t) \in V \to (t \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 t)) Fn 𝒫 X$
12	9 11	mp1i	$⊢ J \in Top \to (t \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 t)) Fn 𝒫 X$
13	1	ntrfval	$⊢ J \in Top \to int (J) = (t \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 t))$
14	3 13	syl5eq	$⊢ J \in Top \to I = (t \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 t))$
15	14	fneq1d	$⊢ J \in Top \to (I Fn 𝒫 X \leftrightarrow (t \in 𝒫 X ⟼ ⋃ (J \cap 𝒫 t)) Fn 𝒫 X)$
16	12 15	mpbird	$⊢ J \in Top \to I Fn 𝒫 X$
17	1	topopn	$⊢ J \in Top \to X \in J$
18	4 5 17	dssmapf1od	$⊢ J \in Top \to D : {𝒫 X}^{𝒫 X} \underset{1-1 onto}{⟶} {𝒫 X}^{𝒫 X}$
19		f1of	$⊢ D : {𝒫 X}^{𝒫 X} \underset{1-1 onto}{⟶} {𝒫 X}^{𝒫 X} \to D : {𝒫 X}^{𝒫 X} ⟶ {𝒫 X}^{𝒫 X}$
20	18 19	syl	$⊢ J \in Top \to D : {𝒫 X}^{𝒫 X} ⟶ {𝒫 X}^{𝒫 X}$
21	1 2	clselmap	$⊢ J \in Top \to K \in ({𝒫 X}^{𝒫 X})$
22	20 21	ffvelrnd	$⊢ J \in Top \to D (K) \in ({𝒫 X}^{𝒫 X})$
23		elmapfn	$⊢ D (K) \in ({𝒫 X}^{𝒫 X}) \to D (K) Fn 𝒫 X$
24	22 23	syl	$⊢ J \in Top \to D (K) Fn 𝒫 X$
25		elpwi	$⊢ t \in 𝒫 X \to t \subseteq X$
26	1	ntrval2	$⊢ (J \in Top \land t \subseteq X) \to int (J) (t) = X ∖ cls (J) (X ∖ t)$
27	25 26	sylan2	$⊢ (J \in Top \land t \in 𝒫 X) \to int (J) (t) = X ∖ cls (J) (X ∖ t)$
28	3	fveq1i	$⊢ I (t) = int (J) (t)$
29	2	fveq1i	$⊢ K (X ∖ t) = cls (J) (X ∖ t)$
30	29	difeq2i	$⊢ X ∖ K (X ∖ t) = X ∖ cls (J) (X ∖ t)$
31	27 28 30	3eqtr4g	$⊢ (J \in Top \land t \in 𝒫 X) \to I (t) = X ∖ K (X ∖ t)$
32	17	adantr	$⊢ (J \in Top \land t \in 𝒫 X) \to X \in J$
33	21	adantr	$⊢ (J \in Top \land t \in 𝒫 X) \to K \in ({𝒫 X}^{𝒫 X})$
34		eqid	$⊢ D (K) = D (K)$
35		simpr	$⊢ (J \in Top \land t \in 𝒫 X) \to t \in 𝒫 X$
36		eqid	$⊢ D (K) (t) = D (K) (t)$
37	4 5 32 33 34 35 36	dssmapfv3d	$⊢ (J \in Top \land t \in 𝒫 X) \to D (K) (t) = X ∖ K (X ∖ t)$
38	31 37	eqtr4d	$⊢ (J \in Top \land t \in 𝒫 X) \to I (t) = D (K) (t)$
39	16 24 38	eqfnfvd	$⊢ J \in Top \to I = D (K)$

Metamath Proof Explorer

Theorem dssmapntrcls

Proof