Metamath Proof Explorer

Theorem neicvgnex

Description: If the neighborhoods and convergents functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021)

Ref Expression
Hypotheses neicvg.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
neicvg.p ⊢ P = n ∈ V ⟼ p ∈ 𝒫 n 𝒫 n ⟼ o ∈ 𝒫 n ⟼ n ∖ p ⁡ n ∖ o
neicvg.d ⊢ D = P ⁡ B
neicvg.f ⊢ F = 𝒫 B O B
neicvg.g ⊢ G = B O 𝒫 B
neicvg.h ⊢ H = F ∘ D ∘ G
neicvg.r ⊢ φ → N H M
Assertion neicvgnex ⊢ φ → N ∈ 𝒫 𝒫 B B

Proof

Step Hyp Ref Expression
1 neicvg.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
2 neicvg.p ⊢ P = n ∈ V ⟼ p ∈ 𝒫 n 𝒫 n ⟼ o ∈ 𝒫 n ⟼ n ∖ p ⁡ n ∖ o
3 neicvg.d ⊢ D = P ⁡ B
4 neicvg.f ⊢ F = 𝒫 B O B
5 neicvg.g ⊢ G = B O 𝒫 B
6 neicvg.h ⊢ H = F ∘ D ∘ G
7 neicvg.r ⊢ φ → N H M
8 1 2 3 4 5 6 7 neicvgnvor ⊢ φ → M H N
9 1 2 3 4 5 6 8 neicvgmex ⊢ φ → N ∈ 𝒫 𝒫 B B