clsneiel2

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then membership in the closure of the complement of a subset is equivalent to the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021)

	Ref	Expression
Hypotheses	clsnei.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
	clsnei.p	$⊢ P = (n \in V ⟼ (p \in ({𝒫 n}^{𝒫 n}) ⟼ (o \in 𝒫 n ⟼ n ∖ p (n ∖ o))))$
	clsnei.d	$⊢ D = P (B)$
	clsnei.f	$⊢ F = 𝒫 B O B$
	clsnei.h	$⊢ H = F \circ D$
	clsnei.r	$⊢ φ \to K H N$
	clsneiel.x	$⊢ φ \to X \in B$
	clsneiel.s	$⊢ φ \to S \in 𝒫 B$
Assertion	clsneiel2	$⊢ φ \to (X \in K (B ∖ S) \leftrightarrow \neg S \in N (X))$

Proof

Step	Hyp	Ref	Expression
1		clsnei.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
2		clsnei.p	$⊢ P = (n \in V ⟼ (p \in ({𝒫 n}^{𝒫 n}) ⟼ (o \in 𝒫 n ⟼ n ∖ p (n ∖ o))))$
3		clsnei.d	$⊢ D = P (B)$
4		clsnei.f	$⊢ F = 𝒫 B O B$
5		clsnei.h	$⊢ H = F \circ D$
6		clsnei.r	$⊢ φ \to K H N$
7		clsneiel.x	$⊢ φ \to X \in B$
8		clsneiel.s	$⊢ φ \to S \in 𝒫 B$
9	3 5 6	clsneircomplex	$⊢ φ \to B ∖ S \in 𝒫 B$
10	1 2 3 4 5 6 7 9	clsneiel1	$⊢ φ \to (X \in K (B ∖ S) \leftrightarrow \neg B ∖ (B ∖ S) \in N (X))$
11	8	elpwid	$⊢ φ \to S \subseteq B$
12		dfss4	$⊢ S \subseteq B \leftrightarrow B ∖ (B ∖ S) = S$
13	11 12	sylib	$⊢ φ \to B ∖ (B ∖ S) = S$
14	13	eleq1d	$⊢ φ \to (B ∖ (B ∖ S) \in N (X) \leftrightarrow S \in N (X))$
15	14	notbid	$⊢ φ \to (\neg B ∖ (B ∖ S) \in N (X) \leftrightarrow \neg S \in N (X))$
16	10 15	bitrd	$⊢ φ \to (X \in K (B ∖ S) \leftrightarrow \neg S \in N (X))$

Metamath Proof Explorer

Theorem clsneiel2

Proof