clsneifv3

Description: Value of the neighborhoods (convergents) in terms of the closure (interior) function. (Contributed by RP, 27-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$
	clsneifv.x	$⊢ φ \to X \in B$
Assertion	clsneifv3	$⊢ φ \to N (X) = \{s \in 𝒫 B \| \neg X \in K (B ∖ s)\}$

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		clsneifv.x	$⊢ φ \to X \in B$
8		dfin5	$⊢ 𝒫 B \cap N (X) = \{s \in 𝒫 B \| s \in N (X)\}$
9	1 2 3 4 5 6	clsneinex	$⊢ φ \to N \in ({𝒫 𝒫 B}^{B})$
10		elmapi	$⊢ N \in ({𝒫 𝒫 B}^{B}) \to N : B ⟶ 𝒫 𝒫 B$
11	9 10	syl	$⊢ φ \to N : B ⟶ 𝒫 𝒫 B$
12	11 7	ffvelcdmd	$⊢ φ \to N (X) \in 𝒫 𝒫 B$
13	12	elpwid	$⊢ φ \to N (X) \subseteq 𝒫 B$
14		sseqin2	$⊢ N (X) \subseteq 𝒫 B \leftrightarrow 𝒫 B \cap N (X) = N (X)$
15	13 14	sylib	$⊢ φ \to 𝒫 B \cap N (X) = N (X)$
16	6	adantr	$⊢ (φ \land s \in 𝒫 B) \to K H N$
17	7	adantr	$⊢ (φ \land s \in 𝒫 B) \to X \in B$
18		simpr	$⊢ (φ \land s \in 𝒫 B) \to s \in 𝒫 B$
19	1 2 3 4 5 16 17 18	clsneiel2	$⊢ (φ \land s \in 𝒫 B) \to (X \in K (B ∖ s) \leftrightarrow \neg s \in N (X))$
20	19	con2bid	$⊢ (φ \land s \in 𝒫 B) \to (s \in N (X) \leftrightarrow \neg X \in K (B ∖ s))$
21	20	rabbidva	$⊢ φ \to \{s \in 𝒫 B \| s \in N (X)\} = \{s \in 𝒫 B \| \neg X \in K (B ∖ s)\}$
22	8 15 21	3eqtr3a	$⊢ φ \to N (X) = \{s \in 𝒫 B \| \neg X \in K (B ∖ s)\}$

Metamath Proof Explorer