Metamath Proof Explorer


Theorem neicvgbex

Description: If (pseudo-)neighborhood and (pseudo-)convergent functions are related by the composite operator, H , then the base set exists. (Contributed by RP, 4-Jun-2021)

Ref Expression
Hypotheses neicvgbex.d D=PB
neicvgbex.h H=FDG
neicvgbex.r φNHM
Assertion neicvgbex φBV

Proof

Step Hyp Ref Expression
1 neicvgbex.d D=PB
2 neicvgbex.h H=FDG
3 neicvgbex.r φNHM
4 1 coeq1i DG=PBG
5 4 coeq2i FDG=FPBG
6 2 5 eqtri H=FPBG
7 6 a1i φH=FPBG
8 7 3 breqdi φNFPBGM
9 brne0 NFPBGMFPBG
10 fvprc ¬BVPB=
11 10 dmeqd ¬BVdomPB=dom
12 dm0 dom=
13 11 12 eqtrdi ¬BVdomPB=
14 13 ineq1d ¬BVdomPBranG=ranG
15 0in ranG=
16 14 15 eqtrdi ¬BVdomPBranG=
17 16 coemptyd ¬BVPBG=
18 17 rneqd ¬BVranPBG=ran
19 rn0 ran=
20 18 19 eqtrdi ¬BVranPBG=
21 20 ineq2d ¬BVdomFranPBG=domF
22 in0 domF=
23 21 22 eqtrdi ¬BVdomFranPBG=
24 23 coemptyd ¬BVFPBG=
25 24 necon1ai FPBGBV
26 8 9 25 3syl φBV