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 IDK$$
Assertion	ntrclscls00	$$⊢\phi \to \left(I\left(B\right)=B\leftrightarrow 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 IDK$$
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	eqtrdi	$$⊢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	eqtrdi	$$⊢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\leftrightarrow K\left(\varnothing \right)=\varnothing \right)$$