Metamath Proof Explorer


Theorem ntrelmap

Description: The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021)

Ref Expression
Hypotheses ntrrn.x 𝑋 = 𝐽
ntrrn.i 𝐼 = ( int ‘ 𝐽 )
Assertion ntrelmap ( 𝐽 ∈ Top → 𝐼 ∈ ( 𝒫 𝑋m 𝒫 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ntrrn.x 𝑋 = 𝐽
2 ntrrn.i 𝐼 = ( int ‘ 𝐽 )
3 1 2 ntrf2 ( 𝐽 ∈ Top → 𝐼 : 𝒫 𝑋 ⟶ 𝒫 𝑋 )
4 1 topopn ( 𝐽 ∈ Top → 𝑋𝐽 )
5 4 pwexd ( 𝐽 ∈ Top → 𝒫 𝑋 ∈ V )
6 5 5 elmapd ( 𝐽 ∈ Top → ( 𝐼 ∈ ( 𝒫 𝑋m 𝒫 𝑋 ) ↔ 𝐼 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) )
7 3 6 mpbird ( 𝐽 ∈ Top → 𝐼 ∈ ( 𝒫 𝑋m 𝒫 𝑋 ) )