Metamath Proof Explorer


Theorem ntrclselnel2

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is an equivalence between membership in interior of the complement of a set and non-membership in the closure of the set. (Contributed by RP, 28-May-2021)

Ref Expression
Hypotheses ntrcls.o 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖𝑗 ) ) ) ) ) )
ntrcls.d 𝐷 = ( 𝑂𝐵 )
ntrcls.r ( 𝜑𝐼 𝐷 𝐾 )
ntrcls.x ( 𝜑𝑋𝐵 )
ntrcls.s ( 𝜑𝑆 ∈ 𝒫 𝐵 )
Assertion ntrclselnel2 ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ ( 𝐵𝑆 ) ) ↔ ¬ 𝑋 ∈ ( 𝐾𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖𝑗 ) ) ) ) ) )
2 ntrcls.d 𝐷 = ( 𝑂𝐵 )
3 ntrcls.r ( 𝜑𝐼 𝐷 𝐾 )
4 ntrcls.x ( 𝜑𝑋𝐵 )
5 ntrcls.s ( 𝜑𝑆 ∈ 𝒫 𝐵 )
6 1 2 3 ntrclsnvobr ( 𝜑𝐾 𝐷 𝐼 )
7 1 2 6 4 5 ntrclselnel1 ( 𝜑 → ( 𝑋 ∈ ( 𝐾𝑆 ) ↔ ¬ 𝑋 ∈ ( 𝐼 ‘ ( 𝐵𝑆 ) ) ) )
8 7 con2bid ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ ( 𝐵𝑆 ) ) ↔ ¬ 𝑋 ∈ ( 𝐾𝑆 ) ) )