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 𝒫 𝑋 ) )