Metamath Proof Explorer

Theorem clsneiel2

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then membership in the closure of the complement of a subset is equivalent to the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021)

Ref Expression
Hypotheses clsnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
clsnei.p ⊢ P = n ∈ V ⟼ p ∈ 𝒫 n 𝒫 n ⟼ o ∈ 𝒫 n ⟼ n ∖ p ⁡ n ∖ o
clsnei.d ⊢ D = P ⁡ B
clsnei.f ⊢ F = 𝒫 B O B
clsnei.h ⊢ H = F ∘ D
clsnei.r ⊢ φ → K H N
clsneiel.x ⊢ φ → X ∈ B
clsneiel.s ⊢ φ → S ∈ 𝒫 B
Assertion clsneiel2 ⊢ φ → X ∈ K ⁡ B ∖ S ↔ ¬ S ∈ N ⁡ X

Proof

Step Hyp Ref Expression
1 clsnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
2 clsnei.p ⊢ P = n ∈ V ⟼ p ∈ 𝒫 n 𝒫 n ⟼ o ∈ 𝒫 n ⟼ n ∖ p ⁡ n ∖ o
3 clsnei.d ⊢ D = P ⁡ B
4 clsnei.f ⊢ F = 𝒫 B O B
5 clsnei.h ⊢ H = F ∘ D
6 clsnei.r ⊢ φ → K H N
7 clsneiel.x ⊢ φ → X ∈ B
8 clsneiel.s ⊢ φ → S ∈ 𝒫 B
9 3 5 6 clsneircomplex ⊢ φ → B ∖ S ∈ 𝒫 B
10 1 2 3 4 5 6 7 9 clsneiel1 ⊢ φ → X ∈ K ⁡ B ∖ S ↔ ¬ B ∖ B ∖ S ∈ N ⁡ X
11 8 elpwid ⊢ φ → S ⊆ B
12 dfss4 ⊢ S ⊆ B ↔ B ∖ B ∖ S = S
13 11 12 sylib ⊢ φ → B ∖ B ∖ S = S
14 13 eleq1d ⊢ φ → B ∖ B ∖ S ∈ N ⁡ X ↔ S ∈ N ⁡ X
15 14 notbid ⊢ φ → ¬ B ∖ B ∖ S ∈ N ⁡ X ↔ ¬ S ∈ N ⁡ X
16 10 15 bitrd ⊢ φ → X ∈ K ⁡ B ∖ S ↔ ¬ S ∈ N ⁡ X