Definition df-ntr 12696

Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 12710. (Contributed by NM, 10-Sep-2006.)

Assertion

Ref	Expression
df-ntr	⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))

Distinct variable group:   𝑥,𝑗

Detailed syntax breakdown of Definition df-ntr

Step	Hyp	Ref	Expression
1		cnt 12693	. 2 class int
2		vj	. . 3 setvar 𝑗
3		ctop 12595	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1342	. . . . . 6 class 𝑗
6	5	cuni 3788	. . . . 5 class ∪ 𝑗
7	6	cpw 3558	. . . 4 class 𝒫 ∪ 𝑗
8	4	cv 1342	. . . . . . 7 class 𝑥
9	8	cpw 3558	. . . . . 6 class 𝒫 𝑥
10	5, 9	cin 3114	. . . . 5 class (𝑗 ∩ 𝒫 𝑥)
11	10	cuni 3788	. . . 4 class ∪ (𝑗 ∩ 𝒫 𝑥)
12	4, 7, 11	cmpt 4042	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥))
13	2, 3, 12	cmpt 4042	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))
14	1, 13	wceq 1343	1 wff int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))

This definition is referenced by:  ntrfval  12700