Metamath Proof Explorer

Theorem ntrclsfveq

Description: If interior and closure functions are related then equality of a pair of function values is equivalent to equality of a pair of the other function's values. (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.t	$⊢ φ \to T \in 𝒫 B$
	Assertion	ntrclsfveq	$⊢ φ \to (I (S) = I (T) \leftrightarrow K (B ∖ S) = K (B ∖ T))$

Proof

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.t	$⊢ φ \to T \in 𝒫 B$
6	1 2 3 5	ntrclsfv	$⊢ φ \to I (T) = B ∖ K (B ∖ T)$
7	6	eqeq2d	$⊢ φ \to (I (S) = I (T) \leftrightarrow I (S) = B ∖ K (B ∖ T))$
8	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ K (B ∖ T) \in 𝒫 B$
9	1 2 3 4 8	ntrclsfveq1	$⊢ φ \to (I (S) = B ∖ K (B ∖ T) \leftrightarrow K (B ∖ S) = B ∖ (B ∖ K (B ∖ T)))$
10	1 2 3	ntrclskex	$⊢ φ \to K \in ({𝒫 B}^{𝒫 B})$
11		elmapi	$⊢ K \in ({𝒫 B}^{𝒫 B}) \to K : 𝒫 B ⟶ 𝒫 B$
12	10 11	syl	$⊢ φ \to K : 𝒫 B ⟶ 𝒫 B$
13	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ T \in 𝒫 B$
14	12 13	ffvelrnd	$⊢ φ \to K (B ∖ T) \in 𝒫 B$
15	14	elpwid	$⊢ φ \to K (B ∖ T) \subseteq B$
16		dfss4	$⊢ K (B ∖ T) \subseteq B \leftrightarrow B ∖ (B ∖ K (B ∖ T)) = K (B ∖ T)$
17	15 16	sylib	$⊢ φ \to B ∖ (B ∖ K (B ∖ T)) = K (B ∖ T)$
18	17	eqeq2d	$⊢ φ \to (K (B ∖ S) = B ∖ (B ∖ K (B ∖ T)) \leftrightarrow K (B ∖ S) = K (B ∖ T))$
19	7 9 18	3bitrd	$⊢ φ \to (I (S) = I (T) \leftrightarrow K (B ∖ S) = K (B ∖ T))$