Metamath Proof Explorer


Theorem ntrclsneine0

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

Ref Expression
Hypotheses ntrcls.o 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖𝑗 ) ) ) ) ) )
ntrcls.d 𝐷 = ( 𝑂𝐵 )
ntrcls.r ( 𝜑𝐼 𝐷 𝐾 )
Assertion ntrclsneine0 ( 𝜑 → ( ∀ 𝑥𝐵𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼𝑠 ) ↔ ∀ 𝑥𝐵𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ ( 𝐾𝑠 ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖𝑗 ) ) ) ) ) )
2 ntrcls.d 𝐷 = ( 𝑂𝐵 )
3 ntrcls.r ( 𝜑𝐼 𝐷 𝐾 )
4 3 adantr ( ( 𝜑𝑥𝐵 ) → 𝐼 𝐷 𝐾 )
5 simpr ( ( 𝜑𝑥𝐵 ) → 𝑥𝐵 )
6 1 2 4 5 ntrclsneine0lem ( ( 𝜑𝑥𝐵 ) → ( ∃ 𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼𝑠 ) ↔ ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ ( 𝐾𝑠 ) ) )
7 6 ralbidva ( 𝜑 → ( ∀ 𝑥𝐵𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼𝑠 ) ↔ ∀ 𝑥𝐵𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ ( 𝐾𝑠 ) ) )