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∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
ntrnei.f ⊢F=𝒫BOB
ntrnei.r ⊢φ→IFN
Assertion ntrneifv2 ⊢φ→F-1⁡N=I

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
2 ntrnei.f ⊢F=𝒫BOB
3 ntrnei.r ⊢φ→IFN
4 1 2 3 ntrneif1o ⊢φ→F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB
5 1 2 3 ntrneinex ⊢φ→N∈𝒫𝒫BB
6 dff1o3 ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB↔F:𝒫B𝒫B⟶onto𝒫𝒫BB∧Fun⁡F-1
7 6 simprbi ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB→Fun⁡F-1
8 7 adantr ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB∧N∈𝒫𝒫BB→Fun⁡F-1
9 df-rn ⊢ran⁡F=dom⁡F-1
10 f1ofo ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB→F:𝒫B𝒫B⟶onto𝒫𝒫BB
11 forn ⊢F:𝒫B𝒫B⟶onto𝒫𝒫BB→ran⁡F=𝒫𝒫BB
12 10 11 syl ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB→ran⁡F=𝒫𝒫BB
13 9 12 eqtr3id ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB→dom⁡F-1=𝒫𝒫BB
14 13 eleq2d ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB→N∈dom⁡F-1↔N∈𝒫𝒫BB
15 14 biimpar ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB∧N∈𝒫𝒫BB→N∈dom⁡F-1
16 8 15 jca ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB∧N∈𝒫𝒫BB→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↔NF-1I
19 17 18 syl ⊢φ→F-1⁡N=I↔NF-1I
20 1 2 3 ntrneiiex ⊢φ→I∈𝒫B𝒫B
21 brcnvg ⊢N∈𝒫𝒫BB∧I∈𝒫B𝒫B→NF-1I↔IFN
22 5 20 21 syl2anc ⊢φ→NF-1I↔IFN
23 19 22 bitrd ⊢φ→F-1⁡N=I↔IFN
24 3 23 mpbird ⊢φ→F-1⁡N=I