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 ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
clsnei.p ⊢ P = n ∈ V ⟼ p ∈ 𝒫 n 𝒫 n ⟼ o ∈ 𝒫 n ⟼ n ∖ p ⁡ n ∖ o
clsnei.d ⊢ D = P ⁡ B
clsnei.f ⊢ F = 𝒫 B O B
clsnei.h ⊢ H = F ∘ D
clsnei.r ⊢ φ → K H N
Assertion clsneinex ⊢ φ → N ∈ 𝒫 𝒫 B B

Proof

Step Hyp Ref Expression
1 clsnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
2 clsnei.p ⊢ P = n ∈ V ⟼ p ∈ 𝒫 n 𝒫 n ⟼ o ∈ 𝒫 n ⟼ n ∖ p ⁡ n ∖ o
3 clsnei.d ⊢ D = P ⁡ B
4 clsnei.f ⊢ F = 𝒫 B O B
5 clsnei.h ⊢ H = F ∘ D
6 clsnei.r ⊢ φ → K H N
7 3 5 6 clsneibex ⊢ φ → B ∈ V
8 pwexg ⊢ B ∈ V → 𝒫 B ∈ V
9 8 adantl ⊢ φ ∧ B ∈ V → 𝒫 B ∈ V
10 simpr ⊢ φ ∧ B ∈ V → B ∈ V
11 1 9 10 4 fsovf1od ⊢ φ ∧ B ∈ V → F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B
12 f1ofn ⊢ F : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 𝒫 B B → F Fn 𝒫 B 𝒫 B
13 11 12 syl ⊢ φ ∧ B ∈ V → F Fn 𝒫 B 𝒫 B
14 2 3 10 dssmapf1od ⊢ φ ∧ B ∈ V → D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B
15 f1of ⊢ D : 𝒫 B 𝒫 B ⟶ 1-1 onto 𝒫 B 𝒫 B → D : 𝒫 B 𝒫 B ⟶ 𝒫 B 𝒫 B
16 14 15 syl ⊢ φ ∧ B ∈ V → D : 𝒫 B 𝒫 B ⟶ 𝒫 B 𝒫 B
17 6 adantr ⊢ φ ∧ B ∈ V → K H N
18 5 breqi ⊢ K H N ↔ K F ∘ D N
19 17 18 sylib ⊢ φ ∧ B ∈ V → K F ∘ D N
20 13 16 19 brcoffn ⊢ φ ∧ B ∈ V → K D D ⁡ K ∧ D ⁡ K F N
21 7 20 mpdan ⊢ φ → K D D ⁡ K ∧ D ⁡ K F N
22 21 simprd ⊢ φ → D ⁡ K F N
23 1 4 22 ntrneinex ⊢ φ → N ∈ 𝒫 𝒫 B B