Metamath Proof Explorer

Theorem clsneif1o

Description: If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the H operator, then the operator is a one-to-one, onto mapping. (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 clsneif1o 
|- ( ph -> H : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m 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 3 5 6 clsneibex 
 |-  ( ph -> B e. _V )
8 pwexg 
 |-  ( B e. _V -> ~P B e. _V )
9 8 adantl 
 |-  ( ( ph /\ B e. _V ) -> ~P B e. _V )
10 simpr 
 |-  ( ( ph /\ B e. _V ) -> B e. _V )
11 eqid 
 |-  ( ~P B O B ) = ( ~P B O B )
12 1 9 10 11 fsovf1od 
 |-  ( ( ph /\ B e. _V ) -> ( ~P B O B ) : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
13 eqid 
 |-  ( P ` B ) = ( P ` B )
14 2 13 10 dssmapf1od 
 |-  ( ( ph /\ B e. _V ) -> ( P ` B ) : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )
15 f1oco 
 |-  ( ( ( ~P B O B ) : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) /\ ( P ` B ) : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) ) -> ( ( ~P B O B ) o. ( P ` B ) ) : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
16 12 14 15 syl2anc 
 |-  ( ( ph /\ B e. _V ) -> ( ( ~P B O B ) o. ( P ` B ) ) : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
17 7 16 mpdan 
 |-  ( ph -> ( ( ~P B O B ) o. ( P ` B ) ) : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
18 4 3 coeq12i 
 |-  ( F o. D ) = ( ( ~P B O B ) o. ( P ` B ) )
19 5 18 eqtri 
 |-  H = ( ( ~P B O B ) o. ( P ` B ) )
20 f1oeq1 
 |-  ( H = ( ( ~P B O B ) o. ( P ` B ) ) -> ( H : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) <-> ( ( ~P B O B ) o. ( P ` B ) ) : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) ) )
21 19 20 ax-mp 
 |-  ( H : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) <-> ( ( ~P B O B ) o. ( P ` B ) ) : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
22 17 21 sylibr 
 |-  ( ph -> H : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )