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	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vx	$$setvarx$$
4	1	cv	$$setvarj$$
5	4	cuni	$$class\bigcup j$$
6	5	cpw	$$class𝒫\bigcup j$$
7	3	cv	$$setvarx$$
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)$$