ntrclselnel1

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is an equivalence between membership in the interior of a set and non-membership in the closure of the complement of the set. (Contributed by RP, 28-May-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$
	ntrcls.x	$⊢ φ \to X \in B$
	ntrcls.s	$⊢ φ \to S \in 𝒫 B$
Assertion	ntrclselnel1	$⊢ φ \to (X \in I (S) \leftrightarrow \neg X \in K (B ∖ S))$

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		ntrcls.x	$⊢ φ \to X \in B$
5		ntrcls.s	$⊢ φ \to S \in 𝒫 B$
6	1 2 3	ntrclsfv2	$⊢ φ \to D (K) = I$
7	6	eqcomd	$⊢ φ \to I = D (K)$
8	7	fveq1d	$⊢ φ \to I (S) = D (K) (S)$
9	2 3	ntrclsbex	$⊢ φ \to B \in V$
10	1 2 3	ntrclskex	$⊢ φ \to K \in ({𝒫 B}^{𝒫 B})$
11		eqid	$⊢ D (K) = D (K)$
12		eqid	$⊢ D (K) (S) = D (K) (S)$
13	1 2 9 10 11 5 12	dssmapfv3d	$⊢ φ \to D (K) (S) = B ∖ K (B ∖ S)$
14	8 13	eqtrd	$⊢ φ \to I (S) = B ∖ K (B ∖ S)$
15	14	eleq2d	$⊢ φ \to (X \in I (S) \leftrightarrow X \in (B ∖ K (B ∖ S)))$
16		eldif	$⊢ X \in (B ∖ K (B ∖ S)) \leftrightarrow (X \in B \land \neg X \in K (B ∖ S))$
17	16	a1i	$⊢ φ \to (X \in (B ∖ K (B ∖ S)) \leftrightarrow (X \in B \land \neg X \in K (B ∖ S)))$
18	4 17	mpbirand	$⊢ φ \to (X \in (B ∖ K (B ∖ S)) \leftrightarrow \neg X \in K (B ∖ S))$
19	15 18	bitrd	$⊢ φ \to (X \in I (S) \leftrightarrow \neg X \in K (B ∖ S))$

Metamath Proof Explorer

Theorem ntrclselnel1

Proof