Definition df-ntr 22180

Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 22196. (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 22177	. 2 class int
2		vj	. . 3 setvar 𝑗
3		ctop 22051	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1538	. . . . . 6 class 𝑗
6	5	cuni 4840	. . . . 5 class ∪ 𝑗
7	6	cpw 4534	. . . 4 class 𝒫 ∪ 𝑗
8	4	cv 1538	. . . . . . 7 class 𝑥
9	8	cpw 4534	. . . . . 6 class 𝒫 𝑥
10	5, 9	cin 3887	. . . . 5 class (𝑗 ∩ 𝒫 𝑥)
11	10	cuni 4840	. . . 4 class ∪ (𝑗 ∩ 𝒫 𝑥)
12	4, 7, 11	cmpt 5158	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥))
13	2, 3, 12	cmpt 5158	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))
14	1, 13	wceq 1539	1 wff int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))

This definition is referenced by:  ntrfval  22184