Metamath Proof Explorer

Theorem 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 = 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 dssmapntrcls 
|- ( J e. Top -> I = ( D ` K ) )

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 vpwex 
 |-  ~P t e. _V
7 6 inex2 
 |-  ( J i^i ~P t ) e. _V
8 7 uniex 
 |-  U. ( J i^i ~P t ) e. _V
9 8 rgenw 
 |-  A. t e. ~P X U. ( J i^i ~P t ) e. _V
10 nfcv 
 |-  F/_ t ~P X
11 10 fnmptf 
 |-  ( A. t e. ~P X U. ( J i^i ~P t ) e. _V -> ( t e. ~P X |-> U. ( J i^i ~P t ) ) Fn ~P X )
12 9 11 mp1i 
 |-  ( J e. Top -> ( t e. ~P X |-> U. ( J i^i ~P t ) ) Fn ~P X )
13 1 ntrfval 
 |-  ( J e. Top -> ( int ` J ) = ( t e. ~P X |-> U. ( J i^i ~P t ) ) )
14 3 13 syl5eq 
 |-  ( J e. Top -> I = ( t e. ~P X |-> U. ( J i^i ~P t ) ) )
15 14 fneq1d 
 |-  ( J e. Top -> ( I Fn ~P X <-> ( t e. ~P X |-> U. ( J i^i ~P t ) ) Fn ~P X ) )
16 12 15 mpbird 
 |-  ( J e. Top -> I Fn ~P X )
17 1 topopn 
 |-  ( J e. Top -> X e. J )
18 4 5 17 dssmapf1od 
 |-  ( J e. Top -> D : ( ~P X ^m ~P X ) -1-1-onto-> ( ~P X ^m ~P X ) )
19 f1of 
 |-  ( D : ( ~P X ^m ~P X ) -1-1-onto-> ( ~P X ^m ~P X ) -> D : ( ~P X ^m ~P X ) --> ( ~P X ^m ~P X ) )
20 18 19 syl 
 |-  ( J e. Top -> D : ( ~P X ^m ~P X ) --> ( ~P X ^m ~P X ) )
21 1 2 clselmap 
 |-  ( J e. Top -> K e. ( ~P X ^m ~P X ) )
22 20 21 ffvelrnd 
 |-  ( J e. Top -> ( D ` K ) e. ( ~P X ^m ~P X ) )
23 elmapfn 
 |-  ( ( D ` K ) e. ( ~P X ^m ~P X ) -> ( D ` K ) Fn ~P X )
24 22 23 syl 
 |-  ( J e. Top -> ( D ` K ) Fn ~P X )
25 elpwi 
 |-  ( t e. ~P X -> t C_ X )
26 1 ntrval2 
 |-  ( ( J e. Top /\ t C_ X ) -> ( ( int ` J ) ` t ) = ( X \ ( ( cls ` J ) ` ( X \ t ) ) ) )
27 25 26 sylan2 
 |-  ( ( J e. Top /\ t e. ~P X ) -> ( ( 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 e. Top /\ t e. ~P X ) -> ( I ` t ) = ( X \ ( K ` ( X \ t ) ) ) )
32 17 adantr 
 |-  ( ( J e. Top /\ t e. ~P X ) -> X e. J )
33 21 adantr 
 |-  ( ( J e. Top /\ t e. ~P X ) -> K e. ( ~P X ^m ~P X ) )
34 eqid 
 |-  ( D ` K ) = ( D ` K )
35 simpr 
 |-  ( ( J e. Top /\ t e. ~P X ) -> t e. ~P X )
36 eqid 
 |-  ( ( D ` K ) ` t ) = ( ( D ` K ) ` t )
37 4 5 32 33 34 35 36 dssmapfv3d 
 |-  ( ( J e. Top /\ t e. ~P X ) -> ( ( D ` K ) ` t ) = ( X \ ( K ` ( X \ t ) ) ) )
38 31 37 eqtr4d 
 |-  ( ( J e. Top /\ t e. ~P X ) -> ( I ` t ) = ( ( D ` K ) ` t ) )
39 16 24 38 eqfnfvd 
 |-  ( J e. Top -> I = ( D ` K ) )