Metamath Proof Explorer

Theorem clsneifv3

Description: Value of the neighborhoods (convergents) in terms of the closure (interior) 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.x ⊢ φ → X ∈ B
Assertion clsneifv3 ⊢ φ → N ⁡ X = s ∈ 𝒫 B | ¬ X ∈ K ⁡ B ∖ s

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.x ⊢ φ → X ∈ B
8 dfin5 ⊢ 𝒫 B ∩ N ⁡ X = s ∈ 𝒫 B | s ∈ N ⁡ X
9 1 2 3 4 5 6 clsneinex ⊢ φ → N ∈ 𝒫 𝒫 B B
10 elmapi ⊢ N ∈ 𝒫 𝒫 B B → N : B ⟶ 𝒫 𝒫 B
11 9 10 syl ⊢ φ → N : B ⟶ 𝒫 𝒫 B
12 11 7 ffvelcdmd ⊢ φ → N ⁡ X ∈ 𝒫 𝒫 B
13 12 elpwid ⊢ φ → N ⁡ X ⊆ 𝒫 B
14 sseqin2 ⊢ N ⁡ X ⊆ 𝒫 B ↔ 𝒫 B ∩ N ⁡ X = N ⁡ X
15 13 14 sylib ⊢ φ → 𝒫 B ∩ N ⁡ X = N ⁡ X
16 6 adantr ⊢ φ ∧ s ∈ 𝒫 B → K H N
17 7 adantr ⊢ φ ∧ s ∈ 𝒫 B → X ∈ B
18 simpr ⊢ φ ∧ s ∈ 𝒫 B → s ∈ 𝒫 B
19 1 2 3 4 5 16 17 18 clsneiel2 ⊢ φ ∧ s ∈ 𝒫 B → X ∈ K ⁡ B ∖ s ↔ ¬ s ∈ N ⁡ X
20 19 con2bid ⊢ φ ∧ s ∈ 𝒫 B → s ∈ N ⁡ X ↔ ¬ X ∈ K ⁡ B ∖ s
21 20 rabbidva ⊢ φ → s ∈ 𝒫 B | s ∈ N ⁡ X = s ∈ 𝒫 B | ¬ X ∈ K ⁡ B ∖ s
22 8 15 21 3eqtr3a ⊢ φ → N ⁡ X = s ∈ 𝒫 B | ¬ X ∈ K ⁡ B ∖ s