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∈𝒫ji⟼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=𝒫BOB
clsnei.h ⊢H=F∘D
clsnei.r ⊢φ→KHN
Assertion clsneicnv ⊢φ→H-1=D∘BO𝒫B

Proof

Step Hyp Ref Expression
1 clsnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼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=𝒫BOB
5 clsnei.h ⊢H=F∘D
6 clsnei.r ⊢φ→KHN
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 ⊢BO𝒫B=BO𝒫B
16 1 14 11 4 15 fsovcnvd ⊢φ∧B∈V→F-1=BO𝒫B
17 12 16 coeq12d ⊢φ∧B∈V→D-1∘F-1=D∘BO𝒫B
18 10 17 mpdan ⊢φ→D-1∘F-1=D∘BO𝒫B
19 9 18 eqtrid ⊢φ→H-1=D∘BO𝒫B