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 ↦ ( 𝑥 ∈ 𝒫 𝑗 ( 𝑗 ∩ 𝒫 𝑥 ) ) )