Theorem neicvgnvor

Description: If neighborhood and convergent functions are related by operator H , the relationship holds with the functions swapped. (Contributed by RP, 11-Jun-2021)

	Ref	Expression
Hypotheses	neicvg.o	|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
	neicvg.p	|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
	neicvg.d	|- D = ( P ` B )
	neicvg.f	|- F = ( ~P B O B )
	neicvg.g	|- G = ( B O ~P B )
	neicvg.h	|- H = ( F o. ( D o. G ) )
	neicvg.r	|- ( ph -> N H M )
Assertion	neicvgnvor	|- ( ph -> M H N )

Proof

Step	Hyp	Ref	Expression
1		neicvg.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		neicvg.p	|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
3		neicvg.d	|- D = ( P ` B )
4		neicvg.f	|- F = ( ~P B O B )
5		neicvg.g	|- G = ( B O ~P B )
6		neicvg.h	|- H = ( F o. ( D o. G ) )
7		neicvg.r	|- ( ph -> N H M )
8	1 2 3 4 5 6 7	neicvgnvo	|- ( ph -> `' H = H )
9	8	breqd	|- ( ph -> ( N `' H M <-> N H M ) )
10	7 9	mpbird	|- ( ph -> N `' H M )
11		relco	|- Rel ( F o. ( D o. G ) )
12	6	releqi	|- ( Rel H <-> Rel ( F o. ( D o. G ) ) )
13	11 12	mpbir	|- Rel H
14	13	relbrcnv	|- ( N `' H M <-> M H N )
15	10 14	sylib	|- ( ph -> M H N )