Metamath Proof Explorer

Theorem neicvgnvo

Description: If neighborhood and convergent functions are related by operator H , it is its own converse function. (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 neicvgnvo 
|- ( ph -> `' H = H )

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 6 cnveqi 
 |-  `' H = `' ( F o. ( D o. G ) )
9 cnvco 
 |-  `' ( F o. ( D o. G ) ) = ( `' ( D o. G ) o. `' F )
10 cnvco 
 |-  `' ( D o. G ) = ( `' G o. `' D )
11 10 coeq1i 
 |-  ( `' ( D o. G ) o. `' F ) = ( ( `' G o. `' D ) o. `' F )
12 8 9 11 3eqtri 
 |-  `' H = ( ( `' G o. `' D ) o. `' F )
13 3 6 7 neicvgbex 
 |-  ( ph -> B e. _V )
14 13 pwexd 
 |-  ( ph -> ~P B e. _V )
15 1 13 14 5 4 fsovcnvd 
 |-  ( ph -> `' G = F )
16 2 3 13 dssmapnvod 
 |-  ( ph -> `' D = D )
17 15 16 coeq12d 
 |-  ( ph -> ( `' G o. `' D ) = ( F o. D ) )
18 1 14 13 4 5 fsovcnvd 
 |-  ( ph -> `' F = G )
19 17 18 coeq12d 
 |-  ( ph -> ( ( `' G o. `' D ) o. `' F ) = ( ( F o. D ) o. G ) )
20 12 19 syl5eq 
 |-  ( ph -> `' H = ( ( F o. D ) o. G ) )
21 coass 
 |-  ( ( F o. D ) o. G ) = ( F o. ( D o. G ) )
22 21 6 eqtr4i 
 |-  ( ( F o. D ) o. G ) = H
23 20 22 eqtrdi 
 |-  ( ph -> `' H = H )