Metamath Proof Explorer

Theorem ntrneibex

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the base set 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 ntrneibex ⊢ φ → B ∈ V

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 oveq2 ⊢ i = a → 𝒫 j i = 𝒫 j a
5 rabeq ⊢ i = a → m ∈ i | l ∈ k ⁡ m = m ∈ a | l ∈ k ⁡ m
6 5 mpteq2dv ⊢ i = a → l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m = l ∈ j ⟼ m ∈ a | l ∈ k ⁡ m
7 4 6 mpteq12dv ⊢ i = a → k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m = k ∈ 𝒫 j a ⟼ l ∈ j ⟼ m ∈ a | l ∈ k ⁡ m
8 pweq ⊢ j = b → 𝒫 j = 𝒫 b
9 8 oveq1d ⊢ j = b → 𝒫 j a = 𝒫 b a
10 mpteq1 ⊢ j = b → l ∈ j ⟼ m ∈ a | l ∈ k ⁡ m = l ∈ b ⟼ m ∈ a | l ∈ k ⁡ m
11 9 10 mpteq12dv ⊢ j = b → k ∈ 𝒫 j a ⟼ l ∈ j ⟼ m ∈ a | l ∈ k ⁡ m = k ∈ 𝒫 b a ⟼ l ∈ b ⟼ m ∈ a | l ∈ k ⁡ m
12 7 11 cbvmpov ⊢ i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m = a ∈ V , b ∈ V ⟼ k ∈ 𝒫 b a ⟼ l ∈ b ⟼ m ∈ a | l ∈ k ⁡ m
13 1 12 eqtri ⊢ O = a ∈ V , b ∈ V ⟼ k ∈ 𝒫 b a ⟼ l ∈ b ⟼ m ∈ a | l ∈ k ⁡ m
14 2 a1i ⊢ φ → F = 𝒫 B O B
15 13 3 14 brovmptimex2 ⊢ φ → B ∈ V