Metamath Proof Explorer

Theorem neicvgel2

Description: The complement of a subset being an element of a neighborhood at a point is equivalent to that subset not being a element of the convergent at that point. (Contributed by RP, 12-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$
		neicvgel.x	$⊢ φ \to X \in B$
		neicvgel.s	$⊢ φ \to S \in 𝒫 B$
	Assertion	neicvgel2	$⊢ φ \to (B ∖ S \in N (X) \leftrightarrow \neg S \in M (X))$

Proof

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		neicvgel.x	$⊢ φ \to X \in B$
9		neicvgel.s	$⊢ φ \to S \in 𝒫 B$
10	3 6 7	neicvgrcomplex	$⊢ φ \to B ∖ S \in 𝒫 B$
11	1 2 3 4 5 6 7 8 10	neicvgel1	$⊢ φ \to (B ∖ S \in N (X) \leftrightarrow \neg B ∖ (B ∖ S) \in M (X))$
12	9	elpwid	$⊢ φ \to S \subseteq B$
13		dfss4	$⊢ S \subseteq B \leftrightarrow B ∖ (B ∖ S) = S$
14	12 13	sylib	$⊢ φ \to B ∖ (B ∖ S) = S$
15	14	eleq1d	$⊢ φ \to (B ∖ (B ∖ S) \in M (X) \leftrightarrow S \in M (X))$
16	15	notbid	$⊢ φ \to (\neg B ∖ (B ∖ S) \in M (X) \leftrightarrow \neg S \in M (X))$
17	11 16	bitrd	$⊢ φ \to (B ∖ S \in N (X) \leftrightarrow \neg S \in M (X))$