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 = j Top x 𝒫 j j 𝒫 x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnt class int
1 vj setvar j
2 ctop class Top
3 vx setvar x
4 1 cv setvar j
5 4 cuni class j
6 5 cpw class 𝒫 j
7 3 cv setvar x
8 7 cpw class 𝒫 x
9 4 8 cin class j 𝒫 x
10 9 cuni class j 𝒫 x
11 3 6 10 cmpt class x 𝒫 j j 𝒫 x
12 1 2 11 cmpt class j Top x 𝒫 j j 𝒫 x
13 0 12 wceq wff int = j Top x 𝒫 j j 𝒫 x