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 | ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ ( 𝐾 ‘ 𝑠 ) ) ) |
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 | ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑠 ∈ 𝒫 𝐵 ¬ 𝑥 ∈ ( 𝐾 ‘ 𝑠 ) ) ) |