Metamath Proof Explorer

Theorem ntrneiiex

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the interior function exists. (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 ntrneiiex ⊢ φ → I ∈ 𝒫 B 𝒫 B

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 f1orel ⊢ F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B → Rel ⁡ F
6 4 5 syl ⊢ φ → Rel ⁡ F
7 releldm ⊢ Rel ⁡ F ∧ I F N → I ∈ dom ⁡ F
8 6 3 7 syl2anc ⊢ φ → I ∈ dom ⁡ F
9 f1odm ⊢ F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B → dom ⁡ F = 𝒫 B 𝒫 B
10 4 9 syl ⊢ φ → dom ⁡ F = 𝒫 B 𝒫 B
11 8 10 eleqtrd ⊢ φ → I ∈ 𝒫 B 𝒫 B