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