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 syl5eqr ⊢ 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