Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Exploring Topology via Seifert and Threlfall
Generic Pseudoclosure Spaces, Pseudointerior Spaces, and Pseudoneighborhoods
ntrclselnel2
Metamath Proof Explorer
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
⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ ( 𝐵 ∖ 𝑆 ) ) ↔ ¬ 𝑋 ∈ ( 𝐾 ‘ 𝑆 ) ) )