Metamath Proof Explorer

Theorem ntrneinex

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the neighborhood 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 ntrneinex ⊢ φ → N ∈ 𝒫 𝒫 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 relelrn ⊢ Rel ⁡ F ∧ I F N → N ∈ ran ⁡ F
8 6 3 7 syl2anc ⊢ φ → N ∈ ran ⁡ F
9 dff1o2 ⊢ F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B ↔ F Fn 𝒫 B 𝒫 B ∧ Fun ⁡ F -1 ∧ ran ⁡ F = 𝒫 𝒫 B B
10 4 9 sylib ⊢ φ → F Fn 𝒫 B 𝒫 B ∧ Fun ⁡ F -1 ∧ ran ⁡ F = 𝒫 𝒫 B B
11 10 simp3d ⊢ φ → ran ⁡ F = 𝒫 𝒫 B B
12 8 11 eleqtrd ⊢ φ → N ∈ 𝒫 𝒫 B B