Metamath Proof Explorer

Theorem clsneifv4

Description: Value of the closure (interior) function in terms of the neighborhoods (convergents) function. (Contributed by RP, 27-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
clsneifv.s ⊢ φ → S ∈ 𝒫 B
Assertion clsneifv4 ⊢ φ → K ⁡ S = x ∈ B | ¬ 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 clsneifv.s ⊢ φ → S ∈ 𝒫 B
8 dfin5 ⊢ B ∩ K ⁡ S = x ∈ B | x ∈ K ⁡ S
9 1 2 3 4 5 6 clsneikex ⊢ φ → K ∈ 𝒫 B 𝒫 B
10 elmapi ⊢ K ∈ 𝒫 B 𝒫 B → K : 𝒫 B ⟶ 𝒫 B
11 9 10 syl ⊢ φ → K : 𝒫 B ⟶ 𝒫 B
12 11 7 ffvelcdmd ⊢ φ → K ⁡ S ∈ 𝒫 B
13 12 elpwid ⊢ φ → K ⁡ S ⊆ B
14 sseqin2 ⊢ K ⁡ S ⊆ B ↔ B ∩ K ⁡ S = K ⁡ S
15 13 14 sylib ⊢ φ → B ∩ K ⁡ S = K ⁡ S
16 6 adantr ⊢ φ ∧ x ∈ B → K H N
17 simpr ⊢ φ ∧ x ∈ B → x ∈ B
18 7 adantr ⊢ φ ∧ x ∈ B → S ∈ 𝒫 B
19 1 2 3 4 5 16 17 18 clsneiel1 ⊢ φ ∧ x ∈ B → x ∈ K ⁡ S ↔ ¬ B ∖ S ∈ N ⁡ x
20 19 rabbidva ⊢ φ → x ∈ B | x ∈ K ⁡ S = x ∈ B | ¬ B ∖ S ∈ N ⁡ x
21 8 15 20 3eqtr3a ⊢ φ → K ⁡ S = x ∈ B | ¬ B ∖ S ∈ N ⁡ x