Definition df-ntr 23028

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

This definition is referenced by:  ntrfval  23032