Database
BASIC TOPOLOGY
Topology
Closure and interior
df-ntr
Metamath Proof Explorer
Description: Define a function on topologies whose value is the interior function on
the subsets of the base set. See ntrval . (Contributed by NM , 10-Sep-2006)
Ref
Expression
Assertion
df-ntr
⊢ int = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ ⋃ j ∩ 𝒫 x
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cnt
class int
1
vj
setvar j
2
ctop
class Top
3
vx
setvar x
4
1
cv
setvar j
5
4
cuni
class ⋃ j
6
5
cpw
class 𝒫 ⋃ j
7
3
cv
setvar x
8
7
cpw
class 𝒫 x
9
4 8
cin
class j ∩ 𝒫 x
10
9
cuni
class ⋃ j ∩ 𝒫 x
11
3 6 10
cmpt
class x ∈ 𝒫 ⋃ j ⟼ ⋃ j ∩ 𝒫 x
12
1 2 11
cmpt
class j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ ⋃ j ∩ 𝒫 x
13
0 12
wceq
wff int = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j ⟼ ⋃ j ∩ 𝒫 x