# 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 ${⊢}\mathrm{int}=\left({j}\in \mathrm{Top}⟼\left({x}\in 𝒫\bigcup {j}⟼\bigcup \left({j}\cap 𝒫{x}\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cnt ${class}\mathrm{int}$
1 vj ${setvar}{j}$
2 ctop ${class}\mathrm{Top}$
3 vx ${setvar}{x}$
4 1 cv ${setvar}{j}$
5 4 cuni ${class}\bigcup {j}$
6 5 cpw ${class}𝒫\bigcup {j}$
7 3 cv ${setvar}{x}$
8 7 cpw ${class}𝒫{x}$
9 4 8 cin ${class}\left({j}\cap 𝒫{x}\right)$
10 9 cuni ${class}\bigcup \left({j}\cap 𝒫{x}\right)$
11 3 6 10 cmpt ${class}\left({x}\in 𝒫\bigcup {j}⟼\bigcup \left({j}\cap 𝒫{x}\right)\right)$
12 1 2 11 cmpt ${class}\left({j}\in \mathrm{Top}⟼\left({x}\in 𝒫\bigcup {j}⟼\bigcup \left({j}\cap 𝒫{x}\right)\right)\right)$
13 0 12 wceq ${wff}\mathrm{int}=\left({j}\in \mathrm{Top}⟼\left({x}\in 𝒫\bigcup {j}⟼\bigcup \left({j}\cap 𝒫{x}\right)\right)\right)$