This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ntr

Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval . (Contributed by NM, 10-Sep-2006)

Ref Expression
Assertion df-ntr int = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ ( 𝑗 ∩ 𝒫 𝑥 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnt ⊢ int
1 vj ⊢ 𝑗
2 ctop ⊢ Top
3 vx ⊢ 𝑥
4 1 cv ⊢ 𝑗
5 4 cuni ⊢ ∪ 𝑗
6 5 cpw ⊢ 𝒫 ∪ 𝑗
7 3 cv ⊢ 𝑥
8 7 cpw ⊢ 𝒫 𝑥
9 4 8 cin ⊢ ( 𝑗 ∩ 𝒫 𝑥 )
10 9 cuni ⊢ ∪ ( 𝑗 ∩ 𝒫 𝑥 )
11 3 6 10 cmpt ⊢ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ ( 𝑗 ∩ 𝒫 𝑥 ) )
12 1 2 11 cmpt ⊢ ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ ( 𝑗 ∩ 𝒫 𝑥 ) ) )
13 0 12 wceq ⊢ int = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ ( 𝑗 ∩ 𝒫 𝑥 ) ) )