Metamath Proof Explorer

Theorem clsneicnv

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then the converse of the operator is known. (Contributed by RP, 5-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
Assertion clsneicnv ⊢ φ → H -1 = D ∘ B O 𝒫 B

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 5 cnveqi ⊢ H -1 = F ∘ D -1
8 cnvco ⊢ F ∘ D -1 = D -1 ∘ F -1
9 7 8 eqtri ⊢ H -1 = D -1 ∘ F -1
10 3 5 6 clsneibex ⊢ φ → B ∈ V
11 simpr ⊢ φ ∧ B ∈ V → B ∈ V
12 2 3 11 dssmapnvod ⊢ φ ∧ B ∈ V → D -1 = D
13 pwexg ⊢ B ∈ V → 𝒫 B ∈ V
14 13 adantl ⊢ φ ∧ B ∈ V → 𝒫 B ∈ V
15 eqid ⊢ B O 𝒫 B = B O 𝒫 B
16 1 14 11 4 15 fsovcnvd ⊢ φ ∧ B ∈ V → F -1 = B O 𝒫 B
17 12 16 coeq12d ⊢ φ ∧ B ∈ V → D -1 ∘ F -1 = D ∘ B O 𝒫 B
18 10 17 mpdan ⊢ φ → D -1 ∘ F -1 = D ∘ B O 𝒫 B
19 9 18 eqtrid ⊢ φ → H -1 = D ∘ B O 𝒫 B