Metamath Proof Explorer

Theorem neicvgf1o

Description: If neighborhood and convergent functions are related by operator H , it is a one-to-one onto relation. (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 neicvgf1o 
|- ( ph -> H : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P ~P B ^m B ) )

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 3 6 7 neicvgbex 
 |-  ( ph -> B e. _V )
9 8 pwexd 
 |-  ( ph -> ~P B e. _V )
10 1 9 8 4 fsovf1od 
 |-  ( ph -> F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
11 2 3 8 dssmapf1od 
 |-  ( ph -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )
12 1 8 9 5 fsovf1od 
 |-  ( ph -> G : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P B ^m ~P B ) )
13 f1oco 
 |-  ( ( D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) /\ G : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P B ^m ~P B ) ) -> ( D o. G ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P B ^m ~P B ) )
14 11 12 13 syl2anc 
 |-  ( ph -> ( D o. G ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P B ^m ~P B ) )
15 f1oco 
 |-  ( ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) /\ ( D o. G ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P B ^m ~P B ) ) -> ( F o. ( D o. G ) ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P ~P B ^m B ) )
16 10 14 15 syl2anc 
 |-  ( ph -> ( F o. ( D o. G ) ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P ~P B ^m B ) )
17 f1oeq1 
 |-  ( H = ( F o. ( D o. G ) ) -> ( H : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P ~P B ^m B ) <-> ( F o. ( D o. G ) ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P ~P B ^m B ) ) )
18 6 17 ax-mp 
 |-  ( H : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P ~P B ^m B ) <-> ( F o. ( D o. G ) ) : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P ~P B ^m B ) )
19 16 18 sylibr 
 |-  ( ph -> H : ( ~P ~P B ^m B ) -1-1-onto-> ( ~P ~P B ^m B ) )