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}=\left({i}\in \mathrm{V},{j}\in \mathrm{V}⟼\left({k}\in \left({𝒫{j}}^{{i}}\right)⟼\left({l}\in {j}⟼\left\{{m}\in {i}|{l}\in {k}\left({m}\right)\right\}\right)\right)\right)$
neicvg.p ${⊢}{P}=\left({n}\in \mathrm{V}⟼\left({p}\in \left({𝒫{n}}^{𝒫{n}}\right)⟼\left({o}\in 𝒫{n}⟼{n}\setminus {p}\left({n}\setminus {o}\right)\right)\right)\right)$
neicvg.d ${⊢}{D}={P}\left({B}\right)$
neicvg.f ${⊢}{F}=𝒫{B}{O}{B}$
neicvg.g ${⊢}{G}={B}{O}𝒫{B}$
neicvg.h ${⊢}{H}={F}\circ \left({D}\circ {G}\right)$
neicvg.r ${⊢}{\phi }\to {N}{H}{M}$
neicvgel.x ${⊢}{\phi }\to {X}\in {B}$
neicvgel.s ${⊢}{\phi }\to {S}\in 𝒫{B}$
Assertion neicvgel2 ${⊢}{\phi }\to \left({B}\setminus {S}\in {N}\left({X}\right)↔¬{S}\in {M}\left({X}\right)\right)$

Proof

Step Hyp Ref Expression
1 neicvg.o ${⊢}{O}=\left({i}\in \mathrm{V},{j}\in \mathrm{V}⟼\left({k}\in \left({𝒫{j}}^{{i}}\right)⟼\left({l}\in {j}⟼\left\{{m}\in {i}|{l}\in {k}\left({m}\right)\right\}\right)\right)\right)$
2 neicvg.p ${⊢}{P}=\left({n}\in \mathrm{V}⟼\left({p}\in \left({𝒫{n}}^{𝒫{n}}\right)⟼\left({o}\in 𝒫{n}⟼{n}\setminus {p}\left({n}\setminus {o}\right)\right)\right)\right)$
3 neicvg.d ${⊢}{D}={P}\left({B}\right)$
4 neicvg.f ${⊢}{F}=𝒫{B}{O}{B}$
5 neicvg.g ${⊢}{G}={B}{O}𝒫{B}$
6 neicvg.h ${⊢}{H}={F}\circ \left({D}\circ {G}\right)$
7 neicvg.r ${⊢}{\phi }\to {N}{H}{M}$
8 neicvgel.x ${⊢}{\phi }\to {X}\in {B}$
9 neicvgel.s ${⊢}{\phi }\to {S}\in 𝒫{B}$
10 3 6 7 neicvgrcomplex ${⊢}{\phi }\to {B}\setminus {S}\in 𝒫{B}$
11 1 2 3 4 5 6 7 8 10 neicvgel1 ${⊢}{\phi }\to \left({B}\setminus {S}\in {N}\left({X}\right)↔¬{B}\setminus \left({B}\setminus {S}\right)\in {M}\left({X}\right)\right)$
12 9 elpwid ${⊢}{\phi }\to {S}\subseteq {B}$
13 dfss4 ${⊢}{S}\subseteq {B}↔{B}\setminus \left({B}\setminus {S}\right)={S}$
14 12 13 sylib ${⊢}{\phi }\to {B}\setminus \left({B}\setminus {S}\right)={S}$
15 14 eleq1d ${⊢}{\phi }\to \left({B}\setminus \left({B}\setminus {S}\right)\in {M}\left({X}\right)↔{S}\in {M}\left({X}\right)\right)$
16 15 notbid ${⊢}{\phi }\to \left(¬{B}\setminus \left({B}\setminus {S}\right)\in {M}\left({X}\right)↔¬{S}\in {M}\left({X}\right)\right)$
17 11 16 bitrd ${⊢}{\phi }\to \left({B}\setminus {S}\in {N}\left({X}\right)↔¬{S}\in {M}\left({X}\right)\right)$