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 V , j V k 𝒫 j i l j m i | l k m
ntrnei.f F = 𝒫 B O B
ntrnei.r φ I F N
Assertion ntrneifv2 φ F -1 N = I

Proof

Step Hyp Ref Expression
1 ntrnei.o O = i V , j V k 𝒫 j i l j m i | l k m
2 ntrnei.f F = 𝒫 B O B
3 ntrnei.r φ I F N
4 1 2 3 ntrneif1o φ F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B
5 1 2 3 ntrneinex φ N 𝒫 𝒫 B B
6 dff1o3 F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B F : 𝒫 B 𝒫 B onto 𝒫 𝒫 B B Fun F -1
7 6 simprbi F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B Fun F -1
8 7 adantr F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B N 𝒫 𝒫 B B Fun F -1
9 df-rn ran F = dom F -1
10 f1ofo F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B F : 𝒫 B 𝒫 B onto 𝒫 𝒫 B B
11 forn F : 𝒫 B 𝒫 B onto 𝒫 𝒫 B B ran F = 𝒫 𝒫 B B
12 10 11 syl F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B ran F = 𝒫 𝒫 B B
13 9 12 eqtr3id F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B dom F -1 = 𝒫 𝒫 B B
14 13 eleq2d F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B N dom F -1 N 𝒫 𝒫 B B
15 14 biimpar F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B N 𝒫 𝒫 B B N dom F -1
16 8 15 jca F : 𝒫 B 𝒫 B 1-1 onto 𝒫 𝒫 B B N 𝒫 𝒫 B B Fun F -1 N dom F -1
17 4 5 16 syl2anc φ Fun F -1 N dom F -1
18 funbrfvb Fun F -1 N dom F -1 F -1 N = I N F -1 I
19 17 18 syl φ F -1 N = I N F -1 I
20 1 2 3 ntrneiiex φ I 𝒫 B 𝒫 B
21 brcnvg N 𝒫 𝒫 B B I 𝒫 B 𝒫 B N F -1 I I F N
22 5 20 21 syl2anc φ N F -1 I I F N
23 19 22 bitrd φ F -1 N = I I F N
24 3 23 mpbird φ F -1 N = I