Theorem dssmapclsntr

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

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

Proof

Step	Hyp	Ref	Expression
1		dssmapclsntr.x	$$⊢X=\bigcup J$$
2		dssmapclsntr.k	$$⊢K=\mathrm{cls}\left(J\right)$$
3		dssmapclsntr.i	$$⊢I=\mathrm{int}\left(J\right)$$
4		dssmapclsntr.o	$$⊢O=\left(b\in \mathrm{V}⟼\left(f\in \left({𝒫b}^{𝒫b}\right)⟼\left(s\in 𝒫b⟼b\setminus f\left(b\setminus s\right)\right)\right)\right)$$
5		dssmapclsntr.d	$$⊢D=O\left(X\right)$$
6	1 2 3 4 5	dssmapntrcls	$$⊢J\in \mathrm{Top}\to I=D\left(K\right)$$
7	6	eqcomd	$$⊢J\in \mathrm{Top}\to D\left(K\right)=I$$
8	1	topopn	$$⊢J\in \mathrm{Top}\to X\in J$$
9	4 5 8	dssmapf1od	$$⊢J\in \mathrm{Top}\to D:{𝒫X}^{𝒫X}\underset{1-1\; onto}{⟶}{𝒫X}^{𝒫X}$$
10	1 2	clselmap	$$⊢J\in \mathrm{Top}\to K\in \left({𝒫X}^{𝒫X}\right)$$
11		f1ocnvfv	$$⊢\left(D:{𝒫X}^{𝒫X}\underset{1-1\; onto}{⟶}{𝒫X}^{𝒫X}\wedge K\in \left({𝒫X}^{𝒫X}\right)\right)\to \left(D\left(K\right)=I\to D^{-1}\left(I\right)=K\right)$$
12	9 10 11	syl2anc	$$⊢J\in \mathrm{Top}\to \left(D\left(K\right)=I\to D^{-1}\left(I\right)=K\right)$$
13	7 12	mpd	$$⊢J\in \mathrm{Top}\to D^{-1}\left(I\right)=K$$
14	4 5 8	dssmapnvod	$$⊢J\in \mathrm{Top}\to D^{-1}=D$$
15	14	fveq1d	$$⊢J\in \mathrm{Top}\to D^{-1}\left(I\right)=D\left(I\right)$$
16	13 15	eqtr3d	$$⊢J\in \mathrm{Top}\to K=D\left(I\right)$$