Metamath Proof Explorer

Theorem clsneinex

Description: If closure and neighborhoods functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021)

Ref Expression
Hypotheses clsnei.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
clsnei.p ⊢ 𝑃 = ( 𝑛 ∈ V ↦ ( 𝑝 ∈ ( 𝒫 𝑛 ↑m 𝒫 𝑛 ) ↦ ( 𝑜 ∈ 𝒫 𝑛 ↦ ( 𝑛 ∖ ( 𝑝 ‘ ( 𝑛 ∖ 𝑜 ) ) ) ) ) )
clsnei.d ⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
clsnei.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
clsnei.h ⊢ 𝐻 = ( 𝐹 ∘ 𝐷 )
clsnei.r ⊢ ( 𝜑 → 𝐾 𝐻 𝑁 )
Assertion clsneinex ( 𝜑 → 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )

Proof

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