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 | |
|
neicvgbex.h | |
||
neicvgbex.r | |
||
Assertion | neicvgbex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neicvgbex.d | |
|
2 | neicvgbex.h | |
|
3 | neicvgbex.r | |
|
4 | 1 | coeq1i | |
5 | 4 | coeq2i | |
6 | 2 5 | eqtri | |
7 | 6 | a1i | |
8 | 7 3 | breqdi | |
9 | brne0 | |
|
10 | fvprc | |
|
11 | 10 | dmeqd | |
12 | dm0 | |
|
13 | 11 12 | eqtrdi | |
14 | 13 | ineq1d | |
15 | 0in | |
|
16 | 14 15 | eqtrdi | |
17 | 16 | coemptyd | |
18 | 17 | rneqd | |
19 | rn0 | |
|
20 | 18 19 | eqtrdi | |
21 | 20 | ineq2d | |
22 | in0 | |
|
23 | 21 22 | eqtrdi | |
24 | 23 | coemptyd | |
25 | 24 | necon1ai | |
26 | 8 9 25 | 3syl | |