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 ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
neicvg.p ⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
neicvg.d ⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
neicvg.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
neicvg.g ⊢ 𝐺 = ( 𝐵 𝑂 𝒫 𝐵 )
neicvg.h ⊢ 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
neicvg.r ⊢ ( 𝜑 → 𝑁 𝐻 𝑀 )
Assertion neicvgmex ( 𝜑 → 𝑀 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )

Proof

Step Hyp Ref Expression
1 neicvg.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2 neicvg.p ⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
3 neicvg.d ⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
4 neicvg.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
5 neicvg.g ⊢ 𝐺 = ( 𝐵 𝑂 𝒫 𝐵 )
6 neicvg.h ⊢ 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
7 neicvg.r ⊢ ( 𝜑 → 𝑁 𝐻 𝑀 )
8 3 6 7 neicvgbex ⊢ ( 𝜑 → 𝐵 ∈ V )
9 pwexg ⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ∈ V )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝒫 𝐵 ∈ V )
11 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
12 1 10 11 4 fsovf1od ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
13 f1ofn ⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
14 12 13 syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
15 2 3 11 dssmapf1od ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
16 f1of ⊢ ( 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
17 15 16 syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
18 1 11 10 5 fsovfd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐺 : ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
19 6 breqi ⊢ ( 𝑁 𝐻 𝑀 ↔ 𝑁 ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) 𝑀 )
20 7 19 sylib ⊢ ( 𝜑 → 𝑁 ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) 𝑀 )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝑁 ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) 𝑀 )
22 14 17 18 21 brcofffn ⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) )
23 8 22 mpdan ⊢ ( 𝜑 → ( 𝑁 𝐺 ( 𝐺 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) ∧ ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 ) )
24 23 simp3d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐺 ‘ 𝑁 ) ) 𝐹 𝑀 )
25 1 4 24 ntrneinex ⊢ ( 𝜑 → 𝑀 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )