Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Exploring Topology via Seifert and Threlfall
Generic Pseudoclosure Spaces, Pseudointerior Spaces, and Pseudoneighborhoods
ntrneif1o
Metamath Proof Explorer
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 𝐵 ) )