Definition df-ntr 13599

Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 13613. (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 13596	. 2 class int
2		vj	. . 3 setvar 𝑗
3		ctop 13500	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1352	. . . . . 6 class 𝑗
6	5	cuni 3810	. . . . 5 class ∪ 𝑗
7	6	cpw 3576	. . . 4 class 𝒫 ∪ 𝑗
8	4	cv 1352	. . . . . . 7 class 𝑥
9	8	cpw 3576	. . . . . 6 class 𝒫 𝑥
10	5, 9	cin 3129	. . . . 5 class (𝑗 ∩ 𝒫 𝑥)
11	10	cuni 3810	. . . 4 class ∪ (𝑗 ∩ 𝒫 𝑥)
12	4, 7, 11	cmpt 4065	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥))
13	2, 3, 12	cmpt 4065	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))
14	1, 13	wceq 1353	1 wff int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))

This definition is referenced by:  ntrfval  13603