Metamath Proof Explorer


Theorem ntrneinex

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the neighborhood function exists. (Contributed by RP, 29-May-2021)

Ref Expression
Hypotheses ntrnei.o 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗m 𝑖 ) ↦ ( 𝑙𝑗 ↦ { 𝑚𝑖𝑙 ∈ ( 𝑘𝑚 ) } ) ) )
ntrnei.f 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
ntrnei.r ( 𝜑𝐼 𝐹 𝑁 )
Assertion ntrneinex ( 𝜑𝑁 ∈ ( 𝒫 𝒫 𝐵m 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗m 𝑖 ) ↦ ( 𝑙𝑗 ↦ { 𝑚𝑖𝑙 ∈ ( 𝑘𝑚 ) } ) ) )
2 ntrnei.f 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3 ntrnei.r ( 𝜑𝐼 𝐹 𝑁 )
4 1 2 3 ntrneif1o ( 𝜑𝐹 : ( 𝒫 𝐵m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵m 𝐵 ) )
5 f1orel ( 𝐹 : ( 𝒫 𝐵m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵m 𝐵 ) → Rel 𝐹 )
6 4 5 syl ( 𝜑 → Rel 𝐹 )
7 relelrn ( ( Rel 𝐹𝐼 𝐹 𝑁 ) → 𝑁 ∈ ran 𝐹 )
8 6 3 7 syl2anc ( 𝜑𝑁 ∈ ran 𝐹 )
9 dff1o2 ( 𝐹 : ( 𝒫 𝐵m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵m 𝐵 ) ↔ ( 𝐹 Fn ( 𝒫 𝐵m 𝒫 𝐵 ) ∧ Fun 𝐹 ∧ ran 𝐹 = ( 𝒫 𝒫 𝐵m 𝐵 ) ) )
10 4 9 sylib ( 𝜑 → ( 𝐹 Fn ( 𝒫 𝐵m 𝒫 𝐵 ) ∧ Fun 𝐹 ∧ ran 𝐹 = ( 𝒫 𝒫 𝐵m 𝐵 ) ) )
11 10 simp3d ( 𝜑 → ran 𝐹 = ( 𝒫 𝒫 𝐵m 𝐵 ) )
12 8 11 eleqtrd ( 𝜑𝑁 ∈ ( 𝒫 𝒫 𝐵m 𝐵 ) )