Metamath Proof Explorer


Theorem ntrneineine0lem

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then conditions equal to claiming that for every point, at least one (pseudo-)neighborbood exists hold equally. (Contributed by RP, 29-May-2021)

Ref Expression
Hypotheses ntrnei.o O=iV,jVk𝒫jiljmi|lkm
ntrnei.f F=𝒫BOB
ntrnei.r φIFN
ntrnei.x φXB
Assertion ntrneineine0lem φs𝒫BXIsNX

Proof

Step Hyp Ref Expression
1 ntrnei.o O=iV,jVk𝒫jiljmi|lkm
2 ntrnei.f F=𝒫BOB
3 ntrnei.r φIFN
4 ntrnei.x φXB
5 3 adantr φs𝒫BIFN
6 4 adantr φs𝒫BXB
7 simpr φs𝒫Bs𝒫B
8 1 2 5 6 7 ntrneiel φs𝒫BXIssNX
9 8 rexbidva φs𝒫BXIss𝒫BsNX
10 1 2 3 ntrneinex φN𝒫𝒫BB
11 elmapi N𝒫𝒫BBN:B𝒫𝒫B
12 10 11 syl φN:B𝒫𝒫B
13 12 4 ffvelrnd φNX𝒫𝒫B
14 13 elpwid φNX𝒫B
15 14 sseld φsNXs𝒫B
16 15 pm4.71rd φsNXs𝒫BsNX
17 16 exbidv φssNXss𝒫BsNX
18 17 bicomd φss𝒫BsNXssNX
19 df-rex s𝒫BsNXss𝒫BsNX
20 n0 NXssNX
21 18 19 20 3bitr4g φs𝒫BsNXNX
22 9 21 bitrd φs𝒫BXIsNX