neicvgfv

Description: The value of the neighborhoods (convergents) in terms of the convergents (neighborhoods) function. (Contributed by RP, 27-Jun-2021)

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

Step	Hyp	Ref	Expression
1		neicvg.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
2		neicvg.p	$⊢ P = (n \in V ⟼ (p \in ({𝒫 n}^{𝒫 n}) ⟼ (o \in 𝒫 n ⟼ n ∖ p (n ∖ o))))$
3		neicvg.d	$⊢ D = P (B)$
4		neicvg.f	$⊢ F = 𝒫 B O B$
5		neicvg.g	$⊢ G = B O 𝒫 B$
6		neicvg.h	$⊢ H = F \circ (D \circ G)$
7		neicvg.r	$⊢ φ \to N H M$
8		neicvgfv.x	$⊢ φ \to X \in B$
9		dfin5	$⊢ 𝒫 B \cap N (X) = \{s \in 𝒫 B \| s \in N (X)\}$
10	1 2 3 4 5 6 7	neicvgnex	$⊢ φ \to N \in ({𝒫 𝒫 B}^{B})$
11		elmapi	$⊢ N \in ({𝒫 𝒫 B}^{B}) \to N : B ⟶ 𝒫 𝒫 B$
12	10 11	syl	$⊢ φ \to N : B ⟶ 𝒫 𝒫 B$
13	12 8	ffvelcdmd	$⊢ φ \to N (X) \in 𝒫 𝒫 B$
14	13	elpwid	$⊢ φ \to N (X) \subseteq 𝒫 B$
15		sseqin2	$⊢ N (X) \subseteq 𝒫 B \leftrightarrow 𝒫 B \cap N (X) = N (X)$
16	14 15	sylib	$⊢ φ \to 𝒫 B \cap N (X) = N (X)$
17	7	adantr	$⊢ (φ \land s \in 𝒫 B) \to N H M$
18	8	adantr	$⊢ (φ \land s \in 𝒫 B) \to X \in B$
19		simpr	$⊢ (φ \land s \in 𝒫 B) \to s \in 𝒫 B$
20	1 2 3 4 5 6 17 18 19	neicvgel1	$⊢ (φ \land s \in 𝒫 B) \to (s \in N (X) \leftrightarrow \neg B ∖ s \in M (X))$
21	20	rabbidva	$⊢ φ \to \{s \in 𝒫 B \| s \in N (X)\} = \{s \in 𝒫 B \| \neg B ∖ s \in M (X)\}$
22	9 16 21	3eqtr3a	$⊢ φ \to N (X) = \{s \in 𝒫 B \| \neg B ∖ s \in M (X)\}$

Metamath Proof Explorer