Metamath Proof Explorer

Theorem ntrneifv2

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the function value of converse of F is the interior function. (Contributed by RP, 29-May-2021)

Ref Expression
Hypotheses ntrnei.o 
|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
ntrnei.f 
|- F = ( ~P B O B )
ntrnei.r 
|- ( ph -> I F N )
Assertion ntrneifv2 
|- ( ph -> ( `' F ` N ) = I )

Proof

Step Hyp Ref Expression
1 ntrnei.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 ntrnei.f 
 |-  F = ( ~P B O B )
3 ntrnei.r 
 |-  ( ph -> I F N )
4 1 2 3 ntrneif1o 
 |-  ( ph -> F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
5 1 2 3 ntrneinex 
 |-  ( ph -> N e. ( ~P ~P B ^m B ) )
6 dff1o3 
 |-  ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) <-> ( F : ( ~P B ^m ~P B ) -onto-> ( ~P ~P B ^m B ) /\ Fun `' F ) )
7 6 simprbi 
 |-  ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> Fun `' F )
8 7 adantr 
 |-  ( ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) /\ N e. ( ~P ~P B ^m B ) ) -> Fun `' F )
9 df-rn 
 |-  ran F = dom `' F
10 f1ofo 
 |-  ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> F : ( ~P B ^m ~P B ) -onto-> ( ~P ~P B ^m B ) )
11 forn 
 |-  ( F : ( ~P B ^m ~P B ) -onto-> ( ~P ~P B ^m B ) -> ran F = ( ~P ~P B ^m B ) )
12 10 11 syl 
 |-  ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> ran F = ( ~P ~P B ^m B ) )
13 9 12 eqtr3id 
 |-  ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> dom `' F = ( ~P ~P B ^m B ) )
14 13 eleq2d 
 |-  ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> ( N e. dom `' F <-> N e. ( ~P ~P B ^m B ) ) )
15 14 biimpar 
 |-  ( ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) /\ N e. ( ~P ~P B ^m B ) ) -> N e. dom `' F )
16 8 15 jca 
 |-  ( ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) /\ N e. ( ~P ~P B ^m B ) ) -> ( Fun `' F /\ N e. dom `' F ) )
17 4 5 16 syl2anc 
 |-  ( ph -> ( Fun `' F /\ N e. dom `' F ) )
18 funbrfvb 
 |-  ( ( Fun `' F /\ N e. dom `' F ) -> ( ( `' F ` N ) = I <-> N `' F I ) )
19 17 18 syl 
 |-  ( ph -> ( ( `' F ` N ) = I <-> N `' F I ) )
20 1 2 3 ntrneiiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
21 brcnvg 
 |-  ( ( N e. ( ~P ~P B ^m B ) /\ I e. ( ~P B ^m ~P B ) ) -> ( N `' F I <-> I F N ) )
22 5 20 21 syl2anc 
 |-  ( ph -> ( N `' F I <-> I F N ) )
23 19 22 bitrd 
 |-  ( ph -> ( ( `' F ` N ) = I <-> I F N ) )
24 3 23 mpbird 
 |-  ( ph -> ( `' F ` N ) = I )