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∈𝒫ji⟼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=𝒫BOB
neicvg.g ⊢G=BO𝒫B
neicvg.h ⊢H=F∘D∘G
neicvg.r ⊢φ→NHM
Assertion neicvgmex ⊢φ→M∈𝒫𝒫BB

Proof

Step Hyp Ref Expression
1 neicvg.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼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=𝒫BOB
5 neicvg.g ⊢G=BO𝒫B
6 neicvg.h ⊢H=F∘D∘G
7 neicvg.r ⊢φ→NHM
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𝒫𝒫BB
13 f1ofn ⊢F:𝒫B𝒫B⟶1-1 onto𝒫𝒫BB→FFn𝒫B𝒫B
14 12 13 syl ⊢φ∧B∈V→FFn𝒫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:𝒫𝒫BB⟶𝒫B𝒫B
19 6 breqi ⊢NHM↔NF∘D∘GM
20 7 19 sylib ⊢φ→NF∘D∘GM
21 20 adantr ⊢φ∧B∈V→NF∘D∘GM
22 14 17 18 21 brcofffn ⊢φ∧B∈V→NGG⁡N∧G⁡NDD⁡G⁡N∧D⁡G⁡NFM
23 8 22 mpdan ⊢φ→NGG⁡N∧G⁡NDD⁡G⁡N∧D⁡G⁡NFM
24 23 simp3d ⊢φ→D⁡G⁡NFM
25 1 4 24 ntrneinex ⊢φ→M∈𝒫𝒫BB