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 = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ ( 𝑗 ∩ 𝒫 𝑥 ) ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cnt
⊢ int
1
vj
⊢ 𝑗
2
ctop
⊢ Top
3
vx
⊢ 𝑥
4
1
cv
⊢ 𝑗
5
4
cuni
⊢ ∪ 𝑗
6
5
cpw
⊢ 𝒫 ∪ 𝑗
7
3
cv
⊢ 𝑥
8
7
cpw
⊢ 𝒫 𝑥
9
4 8
cin
⊢ ( 𝑗 ∩ 𝒫 𝑥 )
10
9
cuni
⊢ ∪ ( 𝑗 ∩ 𝒫 𝑥 )
11
3 6 10
cmpt
⊢ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ ( 𝑗 ∩ 𝒫 𝑥 ) )
12
1 2 11
cmpt
⊢ ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ ( 𝑗 ∩ 𝒫 𝑥 ) ) )
13
0 12
wceq
⊢ int = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ ( 𝑗 ∩ 𝒫 𝑥 ) ) )