Metamath Proof Explorer

Theorem neicvgf1o

Description: If neighborhood and convergent functions are related by operator H , it is a one-to-one onto relation. (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 neicvgf1o ⊢ φ → H : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 𝒫 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 3 6 7 neicvgbex ⊢ φ → B ∈ V
9 8 pwexd ⊢ φ → 𝒫 B ∈ V
10 1 9 8 4 fsovf1od ⊢ φ → F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
11 2 3 8 dssmapf1od ⊢ φ → D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B
12 1 8 9 5 fsovf1od ⊢ φ → G : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 B 𝒫 B
13 f1oco ⊢ D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B ∧ G : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 B 𝒫 B → D ∘ G : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 B 𝒫 B
14 11 12 13 syl2anc ⊢ φ → D ∘ G : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 B 𝒫 B
15 f1oco ⊢ F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B ∧ D ∘ G : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 B 𝒫 B → F ∘ D ∘ G : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 𝒫 B B
16 10 14 15 syl2anc ⊢ φ → F ∘ D ∘ G : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 𝒫 B B
17 f1oeq1 ⊢ H = F ∘ D ∘ G → H : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 𝒫 B B ↔ F ∘ D ∘ G : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 𝒫 B B
18 6 17 ax-mp ⊢ H : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 𝒫 B B ↔ F ∘ D ∘ G : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 𝒫 B B
19 16 18 sylibr ⊢ φ → H : 𝒫 𝒫 B B ⟶ 1-1 onto 𝒫 𝒫 B B