# Metamath Proof Explorer

## Theorem neicvgel1

Description: A subset being an element of a neighborhood of a point is equivalent to the complement of that subset not being a element of the convergent of 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 neicvgel1 ${⊢}{\phi }\to \left({S}\in {N}\left({X}\right)↔¬{B}\setminus {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 neicvgbex ${⊢}{\phi }\to {B}\in \mathrm{V}$
11 simpr ${⊢}\left({\phi }\wedge {B}\in \mathrm{V}\right)\to {B}\in \mathrm{V}$
12 11 pwexd ${⊢}\left({\phi }\wedge {B}\in \mathrm{V}\right)\to 𝒫{B}\in \mathrm{V}$
13 1 12 11 4 fsovf1od ${⊢}\left({\phi }\wedge {B}\in \mathrm{V}\right)\to {F}:{𝒫{B}}^{𝒫{B}}\underset{1-1 onto}{⟶}{𝒫𝒫{B}}^{{B}}$
14 f1ofn ${⊢}{F}:{𝒫{B}}^{𝒫{B}}\underset{1-1 onto}{⟶}{𝒫𝒫{B}}^{{B}}\to {F}Fn\left({𝒫{B}}^{𝒫{B}}\right)$
15 13 14 syl ${⊢}\left({\phi }\wedge {B}\in \mathrm{V}\right)\to {F}Fn\left({𝒫{B}}^{𝒫{B}}\right)$
16 2 3 11 dssmapf1od ${⊢}\left({\phi }\wedge {B}\in \mathrm{V}\right)\to {D}:{𝒫{B}}^{𝒫{B}}\underset{1-1 onto}{⟶}{𝒫{B}}^{𝒫{B}}$
17 f1of ${⊢}{D}:{𝒫{B}}^{𝒫{B}}\underset{1-1 onto}{⟶}{𝒫{B}}^{𝒫{B}}\to {D}:{𝒫{B}}^{𝒫{B}}⟶{𝒫{B}}^{𝒫{B}}$
18 16 17 syl ${⊢}\left({\phi }\wedge {B}\in \mathrm{V}\right)\to {D}:{𝒫{B}}^{𝒫{B}}⟶{𝒫{B}}^{𝒫{B}}$
19 1 11 12 5 fsovfd ${⊢}\left({\phi }\wedge {B}\in \mathrm{V}\right)\to {G}:{𝒫𝒫{B}}^{{B}}⟶{𝒫{B}}^{𝒫{B}}$
20 6 breqi ${⊢}{N}{H}{M}↔{N}\left({F}\circ \left({D}\circ {G}\right)\right){M}$
21 7 20 sylib ${⊢}{\phi }\to {N}\left({F}\circ \left({D}\circ {G}\right)\right){M}$
22 21 adantr ${⊢}\left({\phi }\wedge {B}\in \mathrm{V}\right)\to {N}\left({F}\circ \left({D}\circ {G}\right)\right){M}$
23 15 18 19 22 brcofffn ${⊢}\left({\phi }\wedge {B}\in \mathrm{V}\right)\to \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)$
24 10 23 mpdan ${⊢}{\phi }\to \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)$
25 simpr2 ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)$
26 8 adantr ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to {X}\in {B}$
27 9 adantr ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to {S}\in 𝒫{B}$
28 2 3 25 26 27 ntrclselnel1 ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left({X}\in {G}\left({N}\right)\left({S}\right)↔¬{X}\in {D}\left({G}\left({N}\right)\right)\left({B}\setminus {S}\right)\right)$
29 eqid ${⊢}𝒫{B}{O}{B}=𝒫{B}{O}{B}$
30 simpr1 ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to {N}{G}{G}\left({N}\right)$
31 5 breqi ${⊢}{N}{G}{G}\left({N}\right)↔{N}\left({B}{O}𝒫{B}\right){G}\left({N}\right)$
32 31 a1i ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left({N}{G}{G}\left({N}\right)↔{N}\left({B}{O}𝒫{B}\right){G}\left({N}\right)\right)$
33 10 adantr ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to {B}\in \mathrm{V}$
34 id ${⊢}{B}\in \mathrm{V}\to {B}\in \mathrm{V}$
35 pwexg ${⊢}{B}\in \mathrm{V}\to 𝒫{B}\in \mathrm{V}$
36 eqid ${⊢}{B}{O}𝒫{B}={B}{O}𝒫{B}$
37 1 34 35 36 fsovf1od ${⊢}{B}\in \mathrm{V}\to \left({B}{O}𝒫{B}\right):{𝒫𝒫{B}}^{{B}}\underset{1-1 onto}{⟶}{𝒫{B}}^{𝒫{B}}$
38 33 37 syl ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left({B}{O}𝒫{B}\right):{𝒫𝒫{B}}^{{B}}\underset{1-1 onto}{⟶}{𝒫{B}}^{𝒫{B}}$
39 f1orel ${⊢}\left({B}{O}𝒫{B}\right):{𝒫𝒫{B}}^{{B}}\underset{1-1 onto}{⟶}{𝒫{B}}^{𝒫{B}}\to \mathrm{Rel}\left({B}{O}𝒫{B}\right)$
40 relbrcnvg ${⊢}\mathrm{Rel}\left({B}{O}𝒫{B}\right)\to \left({G}\left({N}\right){\left({B}{O}𝒫{B}\right)}^{-1}{N}↔{N}\left({B}{O}𝒫{B}\right){G}\left({N}\right)\right)$
41 38 39 40 3syl ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left({G}\left({N}\right){\left({B}{O}𝒫{B}\right)}^{-1}{N}↔{N}\left({B}{O}𝒫{B}\right){G}\left({N}\right)\right)$
42 1 34 35 36 29 fsovcnvd ${⊢}{B}\in \mathrm{V}\to {\left({B}{O}𝒫{B}\right)}^{-1}=𝒫{B}{O}{B}$
43 42 breqd ${⊢}{B}\in \mathrm{V}\to \left({G}\left({N}\right){\left({B}{O}𝒫{B}\right)}^{-1}{N}↔{G}\left({N}\right)\left(𝒫{B}{O}{B}\right){N}\right)$
44 33 43 syl ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left({G}\left({N}\right){\left({B}{O}𝒫{B}\right)}^{-1}{N}↔{G}\left({N}\right)\left(𝒫{B}{O}{B}\right){N}\right)$
45 32 41 44 3bitr2d ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left({N}{G}{G}\left({N}\right)↔{G}\left({N}\right)\left(𝒫{B}{O}{B}\right){N}\right)$
46 30 45 mpbid ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to {G}\left({N}\right)\left(𝒫{B}{O}{B}\right){N}$
47 1 29 46 26 27 ntrneiel ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left({X}\in {G}\left({N}\right)\left({S}\right)↔{S}\in {N}\left({X}\right)\right)$
48 simpr3 ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to {D}\left({G}\left({N}\right)\right){F}{M}$
49 difssd ${⊢}{\phi }\to {B}\setminus {S}\subseteq {B}$
50 10 49 sselpwd ${⊢}{\phi }\to {B}\setminus {S}\in 𝒫{B}$
51 50 adantr ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to {B}\setminus {S}\in 𝒫{B}$
52 1 4 48 26 51 ntrneiel ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left({X}\in {D}\left({G}\left({N}\right)\right)\left({B}\setminus {S}\right)↔{B}\setminus {S}\in {M}\left({X}\right)\right)$
53 52 notbid ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left(¬{X}\in {D}\left({G}\left({N}\right)\right)\left({B}\setminus {S}\right)↔¬{B}\setminus {S}\in {M}\left({X}\right)\right)$
54 28 47 53 3bitr3d ${⊢}\left({\phi }\wedge \left({N}{G}{G}\left({N}\right)\wedge {G}\left({N}\right){D}{D}\left({G}\left({N}\right)\right)\wedge {D}\left({G}\left({N}\right)\right){F}{M}\right)\right)\to \left({S}\in {N}\left({X}\right)↔¬{B}\setminus {S}\in {M}\left({X}\right)\right)$
55 24 54 mpdan ${⊢}{\phi }\to \left({S}\in {N}\left({X}\right)↔¬{B}\setminus {S}\in {M}\left({X}\right)\right)$