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