Theorem ntrclsfveq2

Description: If interior and closure functions are related then specific function values are complementary. (Contributed by RP, 27-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$$
	ntrclsfv.s	$$⊢\phi \to S\in 𝒫B$$
	ntrclsfv.c	$$⊢\phi \to C\in 𝒫B$$
Assertion	ntrclsfveq2	$$⊢\phi \to \left(I\left(B\setminus S\right)=C\leftrightarrow K\left(S\right)=B\setminus C\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		ntrclsfv.s	$$⊢\phi \to S\in 𝒫B$$
5		ntrclsfv.c	$$⊢\phi \to C\in 𝒫B$$
6	1 2 3	ntrclsiex	$$⊢\phi \to I\in \left({𝒫B}^{𝒫B}\right)$$
7		elmapi	$$⊢I\in \left({𝒫B}^{𝒫B}\right)\to I:𝒫B⟶𝒫B$$
8	6 7	syl	$$⊢\phi \to I:𝒫B⟶𝒫B$$
9	2 3	ntrclsrcomplex	$$⊢\phi \to B\setminus S\in 𝒫B$$
10	8 9	ffvelcdmd	$$⊢\phi \to I\left(B\setminus S\right)\in 𝒫B$$
11	10	elpwid	$$⊢\phi \to I\left(B\setminus S\right)\subseteq B$$
12	5	elpwid	$$⊢\phi \to C\subseteq B$$
13		rcompleq	$$⊢\left(I\left(B\setminus S\right)\subseteq B\wedge C\subseteq B\right)\to \left(I\left(B\setminus S\right)=C\leftrightarrow B\setminus I\left(B\setminus S\right)=B\setminus C\right)$$
14	11 12 13	syl2anc	$$⊢\phi \to \left(I\left(B\setminus S\right)=C\leftrightarrow B\setminus I\left(B\setminus S\right)=B\setminus C\right)$$
15	1 2 3	ntrclsnvobr	$$⊢\phi \to KDI$$
16	1 2 15 4	ntrclsfv	$$⊢\phi \to K\left(S\right)=B\setminus I\left(B\setminus S\right)$$
17	16	eqeq1d	$$⊢\phi \to \left(K\left(S\right)=B\setminus C\leftrightarrow B\setminus I\left(B\setminus S\right)=B\setminus C\right)$$
18	14 17	bitr4d	$$⊢\phi \to \left(I\left(B\setminus S\right)=C\leftrightarrow K\left(S\right)=B\setminus C\right)$$