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 → 𝐼 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) |
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 → 𝐼 : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) |