Metamath Proof Explorer

Definition 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. ( kGenj ) , 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 π‘˜ ) ) } )