Definition df-ntr 22516

Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 22532. (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 22513	. 2 class int
2		vj	. . 3 setvar 𝑗
3		ctop 22387	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1541	. . . . . 6 class 𝑗
6	5	cuni 4908	. . . . 5 class ∪ 𝑗
7	6	cpw 4602	. . . 4 class 𝒫 ∪ 𝑗
8	4	cv 1541	. . . . . . 7 class 𝑥
9	8	cpw 4602	. . . . . 6 class 𝒫 𝑥
10	5, 9	cin 3947	. . . . 5 class (𝑗 ∩ 𝒫 𝑥)
11	10	cuni 4908	. . . 4 class ∪ (𝑗 ∩ 𝒫 𝑥)
12	4, 7, 11	cmpt 5231	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥))
13	2, 3, 12	cmpt 5231	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))
14	1, 13	wceq 1542	1 wff int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))

This definition is referenced by:  ntrfval  22520