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