Metamath Proof Explorer


Theorem ntrneineine0

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 ( 𝜑𝐼 𝐹 𝑁 )
Assertion ntrneineine0 ( 𝜑 → ( ∀ 𝑥𝐵𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼𝑠 ) ↔ ∀ 𝑥𝐵 ( 𝑁𝑥 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗m 𝑖 ) ↦ ( 𝑙𝑗 ↦ { 𝑚𝑖𝑙 ∈ ( 𝑘𝑚 ) } ) ) )
2 ntrnei.f 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3 ntrnei.r ( 𝜑𝐼 𝐹 𝑁 )
4 3 adantr ( ( 𝜑𝑥𝐵 ) → 𝐼 𝐹 𝑁 )
5 simpr ( ( 𝜑𝑥𝐵 ) → 𝑥𝐵 )
6 1 2 4 5 ntrneineine0lem ( ( 𝜑𝑥𝐵 ) → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼𝑠 ) ↔ ( 𝑁𝑥 ) ≠ ∅ ) )
7 6 ralbidva ( 𝜑 → ( ∀ 𝑥𝐵𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼𝑠 ) ↔ ∀ 𝑥𝐵 ( 𝑁𝑥 ) ≠ ∅ ) )