ntrclsfveq1

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 = (i \in V ⟼ (k \in ({𝒫 i}^{𝒫 i}) ⟼ (j \in 𝒫 i ⟼ i ∖ k (i ∖ j))))$
	ntrcls.d	$⊢ D = O (B)$
	ntrcls.r	$⊢ φ \to I D K$
	ntrclsfv.s	$⊢ φ \to S \in 𝒫 B$
	ntrclsfv.c	$⊢ φ \to C \in 𝒫 B$
Assertion	ntrclsfveq1	$⊢ φ \to (I (S) = C \leftrightarrow K (B ∖ S) = B ∖ C)$

Step	Hyp	Ref	Expression
1		ntrcls.o	$⊢ O = (i \in V ⟼ (k \in ({𝒫 i}^{𝒫 i}) ⟼ (j \in 𝒫 i ⟼ i ∖ k (i ∖ j))))$
2		ntrcls.d	$⊢ D = O (B)$
3		ntrcls.r	$⊢ φ \to I D K$
4		ntrclsfv.s	$⊢ φ \to S \in 𝒫 B$
5		ntrclsfv.c	$⊢ φ \to C \in 𝒫 B$
6	5	elpwid	$⊢ φ \to C \subseteq B$
7		dfss4	$⊢ C \subseteq B \leftrightarrow B ∖ (B ∖ C) = C$
8	6 7	sylib	$⊢ φ \to B ∖ (B ∖ C) = C$
9	8	eqcomd	$⊢ φ \to C = B ∖ (B ∖ C)$
10	9	eqeq2d	$⊢ φ \to (B ∖ K (B ∖ S) = C \leftrightarrow B ∖ K (B ∖ S) = B ∖ (B ∖ C))$
11	1 2 3 4	ntrclsfv	$⊢ φ \to I (S) = B ∖ K (B ∖ S)$
12	11	eqeq1d	$⊢ φ \to (I (S) = C \leftrightarrow B ∖ K (B ∖ S) = C)$
13	1 2 3	ntrclskex	$⊢ φ \to K \in ({𝒫 B}^{𝒫 B})$
14		elmapi	$⊢ K \in ({𝒫 B}^{𝒫 B}) \to K : 𝒫 B ⟶ 𝒫 B$
15	13 14	syl	$⊢ φ \to K : 𝒫 B ⟶ 𝒫 B$
16	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ S \in 𝒫 B$
17	15 16	ffvelrnd	$⊢ φ \to K (B ∖ S) \in 𝒫 B$
18	17	elpwid	$⊢ φ \to K (B ∖ S) \subseteq B$
19		difssd	$⊢ φ \to B ∖ C \subseteq B$
20		rcompleq	$⊢ (K (B ∖ S) \subseteq B \land B ∖ C \subseteq B) \to (K (B ∖ S) = B ∖ C \leftrightarrow B ∖ K (B ∖ S) = B ∖ (B ∖ C))$
21	18 19 20	syl2anc	$⊢ φ \to (K (B ∖ S) = B ∖ C \leftrightarrow B ∖ K (B ∖ S) = B ∖ (B ∖ C))$
22	10 12 21	3bitr4d	$⊢ φ \to (I (S) = C \leftrightarrow K (B ∖ S) = B ∖ C)$

Metamath Proof Explorer