Metamath Proof Explorer

Theorem ntrclscls00

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that the closure of the empty set is the empty set hold equally. (Contributed by RP, 1-Jun-2021)

Ref Expression
Hypotheses ntrcls.o 
|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
ntrcls.d 
|- D = ( O ` B )
ntrcls.r 
|- ( ph -> I D K )
Assertion ntrclscls00 
|- ( ph -> ( ( I ` B ) = B <-> ( K ` (/) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o 
 |-  O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
2 ntrcls.d 
 |-  D = ( O ` B )
3 ntrcls.r 
 |-  ( ph -> I D K )
4 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
5 4 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` (/) ) = ( K ` (/) ) )
6 2 3 ntrclsbex 
 |-  ( ph -> B e. _V )
7 1 2 3 ntrclsiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
8 eqid 
 |-  ( D ` I ) = ( D ` I )
9 0elpw 
 |-  (/) e. ~P B
10 9 a1i 
 |-  ( ph -> (/) e. ~P B )
11 eqid 
 |-  ( ( D ` I ) ` (/) ) = ( ( D ` I ) ` (/) )
12 1 2 6 7 8 10 11 dssmapfv3d 
 |-  ( ph -> ( ( D ` I ) ` (/) ) = ( B \ ( I ` ( B \ (/) ) ) ) )
13 5 12 eqtr3d 
 |-  ( ph -> ( K ` (/) ) = ( B \ ( I ` ( B \ (/) ) ) ) )
14 dif0 
 |-  ( B \ (/) ) = B
15 14 fveq2i 
 |-  ( I ` ( B \ (/) ) ) = ( I ` B )
16 id 
 |-  ( ( I ` B ) = B -> ( I ` B ) = B )
17 15 16 eqtrid 
 |-  ( ( I ` B ) = B -> ( I ` ( B \ (/) ) ) = B )
18 17 difeq2d 
 |-  ( ( I ` B ) = B -> ( B \ ( I ` ( B \ (/) ) ) ) = ( B \ B ) )
19 difid 
 |-  ( B \ B ) = (/)
20 18 19 eqtrdi 
 |-  ( ( I ` B ) = B -> ( B \ ( I ` ( B \ (/) ) ) ) = (/) )
21 13 20 sylan9eq 
 |-  ( ( ph /\ ( I ` B ) = B ) -> ( K ` (/) ) = (/) )
22 pwidg 
 |-  ( B e. _V -> B e. ~P B )
23 6 22 syl 
 |-  ( ph -> B e. ~P B )
24 1 2 3 23 ntrclsfv 
 |-  ( ph -> ( I ` B ) = ( B \ ( K ` ( B \ B ) ) ) )
25 19 fveq2i 
 |-  ( K ` ( B \ B ) ) = ( K ` (/) )
26 id 
 |-  ( ( K ` (/) ) = (/) -> ( K ` (/) ) = (/) )
27 25 26 eqtrid 
 |-  ( ( K ` (/) ) = (/) -> ( K ` ( B \ B ) ) = (/) )
28 27 difeq2d 
 |-  ( ( K ` (/) ) = (/) -> ( B \ ( K ` ( B \ B ) ) ) = ( B \ (/) ) )
29 28 14 eqtrdi 
 |-  ( ( K ` (/) ) = (/) -> ( B \ ( K ` ( B \ B ) ) ) = B )
30 24 29 sylan9eq 
 |-  ( ( ph /\ ( K ` (/) ) = (/) ) -> ( I ` B ) = B )
31 21 30 impbida 
 |-  ( ph -> ( ( I ` B ) = B <-> ( K ` (/) ) = (/) ) )