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 = U. J
	dssmapclsntr.k	|- K = ( cls ` J )
	dssmapclsntr.i	|- I = ( int ` J )
	dssmapclsntr.o	|- O = ( b e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) )
	dssmapclsntr.d	|- D = ( O ` X )
Assertion	dssmapclsntr	|- ( J e. Top -> K = ( D ` I ) )

Proof

Step	Hyp	Ref	Expression
1		dssmapclsntr.x	|- X = U. J
2		dssmapclsntr.k	|- K = ( cls ` J )
3		dssmapclsntr.i	|- I = ( int ` J )
4		dssmapclsntr.o	|- O = ( b e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) )
5		dssmapclsntr.d	|- D = ( O ` X )
6	1 2 3 4 5	dssmapntrcls	|- ( J e. Top -> I = ( D ` K ) )
7	6	eqcomd	|- ( J e. Top -> ( D ` K ) = I )
8	1	topopn	|- ( J e. Top -> X e. J )
9	4 5 8	dssmapf1od	|- ( J e. Top -> D : ( ~P X ^m ~P X ) -1-1-onto-> ( ~P X ^m ~P X ) )
10	1 2	clselmap	|- ( J e. Top -> K e. ( ~P X ^m ~P X ) )
11		f1ocnvfv	|- ( ( D : ( ~P X ^m ~P X ) -1-1-onto-> ( ~P X ^m ~P X ) /\ K e. ( ~P X ^m ~P X ) ) -> ( ( D ` K ) = I -> ( `' D ` I ) = K ) )
12	9 10 11	syl2anc	|- ( J e. Top -> ( ( D ` K ) = I -> ( `' D ` I ) = K ) )
13	7 12	mpd	|- ( J e. Top -> ( `' D ` I ) = K )
14	4 5 8	dssmapnvod	|- ( J e. Top -> `' D = D )
15	14	fveq1d	|- ( J e. Top -> ( `' D ` I ) = ( D ` I ) )
16	13 15	eqtr3d	|- ( J e. Top -> K = ( D ` I ) )