Metamath Proof Explorer

Theorem ntrneifv1

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the function value of F is the neighborhood 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 ntrneifv1 ⊢ φ → F ⁡ I = N

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 f1ofn ⊢ F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B → F Fn 𝒫 B 𝒫 B
6 4 5 syl ⊢ φ → F Fn 𝒫 B 𝒫 B
7 1 2 3 ntrneiiex ⊢ φ → I ∈ 𝒫 B 𝒫 B
8 6 7 jca ⊢ φ → F Fn 𝒫 B 𝒫 B ∧ I ∈ 𝒫 B 𝒫 B
9 fnfun ⊢ F Fn 𝒫 B 𝒫 B → Fun ⁡ F
10 9 adantr ⊢ F Fn 𝒫 B 𝒫 B ∧ I ∈ 𝒫 B 𝒫 B → Fun ⁡ F
11 fndm ⊢ F Fn 𝒫 B 𝒫 B → dom ⁡ F = 𝒫 B 𝒫 B
12 11 eleq2d ⊢ F Fn 𝒫 B 𝒫 B → I ∈ dom ⁡ F ↔ I ∈ 𝒫 B 𝒫 B
13 12 biimpar ⊢ F Fn 𝒫 B 𝒫 B ∧ I ∈ 𝒫 B 𝒫 B → I ∈ dom ⁡ F
14 10 13 jca ⊢ F Fn 𝒫 B 𝒫 B ∧ I ∈ 𝒫 B 𝒫 B → Fun ⁡ F ∧ I ∈ dom ⁡ F
15 funbrfvb ⊢ Fun ⁡ F ∧ I ∈ dom ⁡ F → F ⁡ I = N ↔ I F N
16 8 14 15 3syl ⊢ φ → F ⁡ I = N ↔ I F N
17 3 16 mpbird ⊢ φ → F ⁡ I = N