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 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗m 𝑖 ) ↦ ( 𝑙𝑗 ↦ { 𝑚𝑖𝑙 ∈ ( 𝑘𝑚 ) } ) ) )
ntrnei.f 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
ntrnei.r ( 𝜑𝐼 𝐹 𝑁 )
ntrnei.x ( 𝜑𝑋𝐵 )
Assertion ntrneineine0lem ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼𝑠 ) ↔ ( 𝑁𝑋 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗m 𝑖 ) ↦ ( 𝑙𝑗 ↦ { 𝑚𝑖𝑙 ∈ ( 𝑘𝑚 ) } ) ) )
2 ntrnei.f 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3 ntrnei.r ( 𝜑𝐼 𝐹 𝑁 )
4 ntrnei.x ( 𝜑𝑋𝐵 )
5 3 adantr ( ( 𝜑𝑠 ∈ 𝒫 𝐵 ) → 𝐼 𝐹 𝑁 )
6 4 adantr ( ( 𝜑𝑠 ∈ 𝒫 𝐵 ) → 𝑋𝐵 )
7 simpr ( ( 𝜑𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
8 1 2 5 6 7 ntrneiel ( ( 𝜑𝑠 ∈ 𝒫 𝐵 ) → ( 𝑋 ∈ ( 𝐼𝑠 ) ↔ 𝑠 ∈ ( 𝑁𝑋 ) ) )
9 8 rexbidva ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼𝑠 ) ↔ ∃ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ ( 𝑁𝑋 ) ) )
10 1 2 3 ntrneinex ( 𝜑𝑁 ∈ ( 𝒫 𝒫 𝐵m 𝐵 ) )
11 elmapi ( 𝑁 ∈ ( 𝒫 𝒫 𝐵m 𝐵 ) → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
12 10 11 syl ( 𝜑𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
13 12 4 ffvelrnd ( 𝜑 → ( 𝑁𝑋 ) ∈ 𝒫 𝒫 𝐵 )
14 13 elpwid ( 𝜑 → ( 𝑁𝑋 ) ⊆ 𝒫 𝐵 )
15 14 sseld ( 𝜑 → ( 𝑠 ∈ ( 𝑁𝑋 ) → 𝑠 ∈ 𝒫 𝐵 ) )
16 15 pm4.71rd ( 𝜑 → ( 𝑠 ∈ ( 𝑁𝑋 ) ↔ ( 𝑠 ∈ 𝒫 𝐵𝑠 ∈ ( 𝑁𝑋 ) ) ) )
17 16 exbidv ( 𝜑 → ( ∃ 𝑠 𝑠 ∈ ( 𝑁𝑋 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵𝑠 ∈ ( 𝑁𝑋 ) ) ) )
18 17 bicomd ( 𝜑 → ( ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵𝑠 ∈ ( 𝑁𝑋 ) ) ↔ ∃ 𝑠 𝑠 ∈ ( 𝑁𝑋 ) ) )
19 df-rex ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ ( 𝑁𝑋 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝐵𝑠 ∈ ( 𝑁𝑋 ) ) )
20 n0 ( ( 𝑁𝑋 ) ≠ ∅ ↔ ∃ 𝑠 𝑠 ∈ ( 𝑁𝑋 ) )
21 18 19 20 3bitr4g ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ ( 𝑁𝑋 ) ↔ ( 𝑁𝑋 ) ≠ ∅ ) )
22 9 21 bitrd ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑋 ∈ ( 𝐼𝑠 ) ↔ ( 𝑁𝑋 ) ≠ ∅ ) )