Metamath Proof Explorer


Theorem ntrneif1o

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , we may characterize the relation as part of a 1-to-1 onto function. (Contributed by RP, 29-May-2021)

Ref Expression
Hypotheses ntrnei.o 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗m 𝑖 ) ↦ ( 𝑙𝑗 ↦ { 𝑚𝑖𝑙 ∈ ( 𝑘𝑚 ) } ) ) )
ntrnei.f 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
ntrnei.r ( 𝜑𝐼 𝐹 𝑁 )
Assertion ntrneif1o ( 𝜑𝐹 : ( 𝒫 𝐵m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵m 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗m 𝑖 ) ↦ ( 𝑙𝑗 ↦ { 𝑚𝑖𝑙 ∈ ( 𝑘𝑚 ) } ) ) )
2 ntrnei.f 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3 ntrnei.r ( 𝜑𝐼 𝐹 𝑁 )
4 1 2 3 ntrneibex ( 𝜑𝐵 ∈ V )
5 4 pwexd ( 𝜑 → 𝒫 𝐵 ∈ V )
6 1 5 4 2 fsovf1od ( 𝜑𝐹 : ( 𝒫 𝐵m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵m 𝐵 ) )