Metamath Proof Explorer

Theorem clsneiel1

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then membership in the closure of a subset is equivalent to the complement of 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 clsneiel1 ⊢ φ → X ∈ K ⁡ S ↔ ¬ B ∖ 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 clsneibex ⊢ φ → B ∈ V
10 9 ancli ⊢ φ → φ ∧ B ∈ V
11 simpr ⊢ φ ∧ B ∈ V → B ∈ V
12 11 pwexd ⊢ φ ∧ B ∈ V → 𝒫 B ∈ V
13 1 12 11 4 fsovfd ⊢ φ ∧ B ∈ V → F : 𝒫 B 𝒫 B ⟶ 𝒫 𝒫 B B
14 13 ffnd ⊢ φ ∧ B ∈ V → F Fn 𝒫 B 𝒫 B
15 2 3 11 dssmapf1od ⊢ φ ∧ B ∈ V → D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B
16 f1of ⊢ D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B → D : 𝒫 B 𝒫 B ⟶ 𝒫 B 𝒫 B
17 15 16 syl ⊢ φ ∧ B ∈ V → D : 𝒫 B 𝒫 B ⟶ 𝒫 B 𝒫 B
18 5 breqi ⊢ K H N ↔ K F ∘ D N
19 6 18 sylib ⊢ φ → K F ∘ D N
20 19 adantr ⊢ φ ∧ B ∈ V → K F ∘ D N
21 14 17 20 brcoffn ⊢ φ ∧ B ∈ V → K D D ⁡ K ∧ D ⁡ K F N
22 simprl ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → K D D ⁡ K
23 7 ad2antrr ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → X ∈ B
24 8 ad2antrr ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → S ∈ 𝒫 B
25 2 3 22 23 24 ntrclselnel1 ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → X ∈ K ⁡ S ↔ ¬ X ∈ D ⁡ K ⁡ B ∖ S
26 simprr ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → D ⁡ K F N
27 simplr ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → B ∈ V
28 difssd ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → B ∖ S ⊆ B
29 27 28 sselpwd ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → B ∖ S ∈ 𝒫 B
30 1 4 26 23 29 ntrneiel ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → X ∈ D ⁡ K ⁡ B ∖ S ↔ B ∖ S ∈ N ⁡ X
31 30 notbid ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → ¬ X ∈ D ⁡ K ⁡ B ∖ S ↔ ¬ B ∖ S ∈ N ⁡ X
32 25 31 bitrd ⊢ φ ∧ B ∈ V ∧ K D D ⁡ K ∧ D ⁡ K F N → X ∈ K ⁡ S ↔ ¬ B ∖ S ∈ N ⁡ X
33 10 21 32 syl2anc2 ⊢ φ → X ∈ K ⁡ S ↔ ¬ B ∖ S ∈ N ⁡ X