This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Topology Compactly generated spaces df-kgen
Description: Define the "compact generator", the functor from topological spaces to
compactly generated spaces. Also known as the k-ification operation. A
set is k-open, i.e. x e. ( kGen j ) , iff the preimage of x
is open in all compact Hausdorff spaces. (Contributed by Mario
Carneiro , 20-Mar-2015)
Ref
Expression
Assertion
df-kgen ⊢ 𝑘Gen = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) } )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
ckgen ⊢ 𝑘Gen
1
vj ⊢ 𝑗
2
ctop ⊢ Top
3
vx ⊢ 𝑥
4
1
cv ⊢ 𝑗
5
4
cuni ⊢ ∪ 𝑗
6
5
cpw ⊢ 𝒫 ∪ 𝑗
7
vk ⊢ 𝑘
8
crest ⊢ ↾t
9
7
cv ⊢ 𝑘
10
4 9 8
co ⊢ ( 𝑗 ↾t 𝑘 )
11
ccmp ⊢ Comp
12
10 11
wcel ⊢ ( 𝑗 ↾t 𝑘 ) ∈ Comp
13
3
cv ⊢ 𝑥
14
13 9
cin ⊢ ( 𝑥 ∩ 𝑘 )
15
14 10
wcel ⊢ ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 )
16
12 15
wi ⊢ ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) )
17
16 7 6
wral ⊢ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) )
18
17 3 6
crab ⊢ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) }
19
1 2 18
cmpt ⊢ ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) } )
20
0 19
wceq ⊢ 𝑘Gen = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑘 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝑗 ↾t 𝑘 ) ) } )