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