Metamath Proof Explorer

Theorem neicvgmex

Description: If the neighborhoods and convergents functions are related, the convergents 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 neicvgmex ⊢ φ → M ∈ 𝒫 𝒫 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 pwexg ⊢ B ∈ V → 𝒫 B ∈ V
10 9 adantl ⊢ φ ∧ B ∈ V → 𝒫 B ∈ V
11 simpr ⊢ φ ∧ B ∈ V → B ∈ V
12 1 10 11 4 fsovf1od ⊢ φ ∧ B ∈ V → F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
13 f1ofn ⊢ F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B → F Fn 𝒫 B 𝒫 B
14 12 13 syl ⊢ φ ∧ B ∈ V → F Fn 𝒫 B 𝒫 B
15 2 3 11 dssmapf1od ⊢ φ ∧ B ∈ V → D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B
16 f1of ⊢ D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B → D : 𝒫 B 𝒫 B ⟶ 𝒫 B 𝒫 B
17 15 16 syl ⊢ φ ∧ B ∈ V → D : 𝒫 B 𝒫 B ⟶ 𝒫 B 𝒫 B
18 1 11 10 5 fsovfd ⊢ φ ∧ B ∈ V → G : 𝒫 𝒫 B B ⟶ 𝒫 B 𝒫 B
19 6 breqi ⊢ N H M ↔ N F ∘ D ∘ G M
20 7 19 sylib ⊢ φ → N F ∘ D ∘ G M
21 20 adantr ⊢ φ ∧ B ∈ V → N F ∘ D ∘ G M
22 14 17 18 21 brcofffn ⊢ φ ∧ B ∈ V → N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M
23 8 22 mpdan ⊢ φ → N G G ⁡ N ∧ G ⁡ N D D ⁡ G ⁡ N ∧ D ⁡ G ⁡ N F M
24 23 simp3d ⊢ φ → D ⁡ G ⁡ N F M
25 1 4 24 ntrneinex ⊢ φ → M ∈ 𝒫 𝒫 B B