# 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}=\left({i}\in \mathrm{V}⟼\left({k}\in \left({𝒫{i}}^{𝒫{i}}\right)⟼\left({j}\in 𝒫{i}⟼{i}\setminus {k}\left({i}\setminus {j}\right)\right)\right)\right)$
ntrcls.d ${⊢}{D}={O}\left({B}\right)$
ntrcls.r ${⊢}{\phi }\to {I}{D}{K}$
Assertion ntrclscls00 ${⊢}{\phi }\to \left({I}\left({B}\right)={B}↔{K}\left(\varnothing \right)=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 ntrcls.o ${⊢}{O}=\left({i}\in \mathrm{V}⟼\left({k}\in \left({𝒫{i}}^{𝒫{i}}\right)⟼\left({j}\in 𝒫{i}⟼{i}\setminus {k}\left({i}\setminus {j}\right)\right)\right)\right)$
2 ntrcls.d ${⊢}{D}={O}\left({B}\right)$
3 ntrcls.r ${⊢}{\phi }\to {I}{D}{K}$
4 1 2 3 ntrclsfv1 ${⊢}{\phi }\to {D}\left({I}\right)={K}$
5 4 fveq1d ${⊢}{\phi }\to {D}\left({I}\right)\left(\varnothing \right)={K}\left(\varnothing \right)$
6 2 3 ntrclsbex ${⊢}{\phi }\to {B}\in \mathrm{V}$
7 1 2 3 ntrclsiex ${⊢}{\phi }\to {I}\in \left({𝒫{B}}^{𝒫{B}}\right)$
8 eqid ${⊢}{D}\left({I}\right)={D}\left({I}\right)$
9 0elpw ${⊢}\varnothing \in 𝒫{B}$
10 9 a1i ${⊢}{\phi }\to \varnothing \in 𝒫{B}$
11 eqid ${⊢}{D}\left({I}\right)\left(\varnothing \right)={D}\left({I}\right)\left(\varnothing \right)$
12 1 2 6 7 8 10 11 dssmapfv3d ${⊢}{\phi }\to {D}\left({I}\right)\left(\varnothing \right)={B}\setminus {I}\left({B}\setminus \varnothing \right)$
13 5 12 eqtr3d ${⊢}{\phi }\to {K}\left(\varnothing \right)={B}\setminus {I}\left({B}\setminus \varnothing \right)$
14 dif0 ${⊢}{B}\setminus \varnothing ={B}$
15 14 fveq2i ${⊢}{I}\left({B}\setminus \varnothing \right)={I}\left({B}\right)$
16 id ${⊢}{I}\left({B}\right)={B}\to {I}\left({B}\right)={B}$
17 15 16 syl5eq ${⊢}{I}\left({B}\right)={B}\to {I}\left({B}\setminus \varnothing \right)={B}$
18 17 difeq2d ${⊢}{I}\left({B}\right)={B}\to {B}\setminus {I}\left({B}\setminus \varnothing \right)={B}\setminus {B}$
19 difid ${⊢}{B}\setminus {B}=\varnothing$
20 18 19 syl6eq ${⊢}{I}\left({B}\right)={B}\to {B}\setminus {I}\left({B}\setminus \varnothing \right)=\varnothing$
21 13 20 sylan9eq ${⊢}\left({\phi }\wedge {I}\left({B}\right)={B}\right)\to {K}\left(\varnothing \right)=\varnothing$
22 pwidg ${⊢}{B}\in \mathrm{V}\to {B}\in 𝒫{B}$
23 6 22 syl ${⊢}{\phi }\to {B}\in 𝒫{B}$
24 1 2 3 23 ntrclsfv ${⊢}{\phi }\to {I}\left({B}\right)={B}\setminus {K}\left({B}\setminus {B}\right)$
25 19 fveq2i ${⊢}{K}\left({B}\setminus {B}\right)={K}\left(\varnothing \right)$
26 id ${⊢}{K}\left(\varnothing \right)=\varnothing \to {K}\left(\varnothing \right)=\varnothing$
27 25 26 syl5eq ${⊢}{K}\left(\varnothing \right)=\varnothing \to {K}\left({B}\setminus {B}\right)=\varnothing$
28 27 difeq2d ${⊢}{K}\left(\varnothing \right)=\varnothing \to {B}\setminus {K}\left({B}\setminus {B}\right)={B}\setminus \varnothing$
29 28 14 syl6eq ${⊢}{K}\left(\varnothing \right)=\varnothing \to {B}\setminus {K}\left({B}\setminus {B}\right)={B}$
30 24 29 sylan9eq ${⊢}\left({\phi }\wedge {K}\left(\varnothing \right)=\varnothing \right)\to {I}\left({B}\right)={B}$
31 21 30 impbida ${⊢}{\phi }\to \left({I}\left({B}\right)={B}↔{K}\left(\varnothing \right)=\varnothing \right)$