Metamath Proof Explorer

Theorem neicvgnvor

Description: If neighborhood and convergent functions are related by operator H , the relationship holds with the functions swapped. (Contributed by RP, 11-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 neicvgnvor ⊢ φ → M H N

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 neicvgnvo ⊢ φ → H -1 = H
9 8 breqd ⊢ φ → N H -1 M ↔ N H M
10 7 9 mpbird ⊢ φ → N H -1 M
11 relco ⊢ Rel ⁡ F ∘ D ∘ G
12 6 releqi ⊢ Rel ⁡ H ↔ Rel ⁡ F ∘ D ∘ G
13 11 12 mpbir ⊢ Rel ⁡ H
14 13 relbrcnv ⊢ N H -1 M ↔ M H N
15 10 14 sylib ⊢ φ → M H N