Metamath Proof Explorer


Theorem ntrf2

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 ntrf2 ( 𝐽 ∈ Top → 𝐼 : 𝒫 𝑋 ⟶ 𝒫 𝑋 )

Proof

Step Hyp Ref Expression
1 ntrrn.x 𝑋 = 𝐽
2 ntrrn.i 𝐼 = ( int ‘ 𝐽 )
3 1 2 ntrf ( 𝐽 ∈ Top → 𝐼 : 𝒫 𝑋𝐽 )
4 1 toptopon ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 topgele ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( { ∅ , 𝑋 } ⊆ 𝐽𝐽 ⊆ 𝒫 𝑋 ) )
6 4 5 sylbi ( 𝐽 ∈ Top → ( { ∅ , 𝑋 } ⊆ 𝐽𝐽 ⊆ 𝒫 𝑋 ) )
7 6 simprd ( 𝐽 ∈ Top → 𝐽 ⊆ 𝒫 𝑋 )
8 3 7 fssd ( 𝐽 ∈ Top → 𝐼 : 𝒫 𝑋 ⟶ 𝒫 𝑋 )