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 e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
	clsnei.p	|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
	clsnei.d	|- D = ( P ` B )
	clsnei.f	|- F = ( ~P B O B )
	clsnei.h	|- H = ( F o. D )
	clsnei.r	|- ( ph -> K H N )
Assertion	clsneicnv	|- ( ph -> `' H = ( D o. ( B O ~P B ) ) )

Proof

Step	Hyp	Ref	Expression
1		clsnei.o	|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
2		clsnei.p	|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
3		clsnei.d	|- D = ( P ` B )
4		clsnei.f	|- F = ( ~P B O B )
5		clsnei.h	|- H = ( F o. D )
6		clsnei.r	|- ( ph -> K H N )
7	5	cnveqi	|- `' H = `' ( F o. D )
8		cnvco	|- `' ( F o. D ) = ( `' D o. `' F )
9	7 8	eqtri	|- `' H = ( `' D o. `' F )
10	3 5 6	clsneibex	|- ( ph -> B e. _V )
11		simpr	|- ( ( ph /\ B e. _V ) -> B e. _V )
12	2 3 11	dssmapnvod	|- ( ( ph /\ B e. _V ) -> `' D = D )
13		pwexg	|- ( B e. _V -> ~P B e. _V )
14	13	adantl	|- ( ( ph /\ B e. _V ) -> ~P B e. _V )
15		eqid	|- ( B O ~P B ) = ( B O ~P B )
16	1 14 11 4 15	fsovcnvd	|- ( ( ph /\ B e. _V ) -> `' F = ( B O ~P B ) )
17	12 16	coeq12d	|- ( ( ph /\ B e. _V ) -> ( `' D o. `' F ) = ( D o. ( B O ~P B ) ) )
18	10 17	mpdan	|- ( ph -> ( `' D o. `' F ) = ( D o. ( B O ~P B ) ) )
19	9 18	eqtrid	|- ( ph -> `' H = ( D o. ( B O ~P B ) ) )