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 = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j | ∀ k ∈ 𝒫 ⋃ j j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k

Detailed syntax breakdown

Step Hyp Ref Expression
0 ckgen class 𝑘Gen
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 vk setvar k
8 crest class ↾ 𝑡
9 7 cv setvar k
10 4 9 8 co class j ↾ 𝑡 k
11 ccmp class Comp
12 10 11 wcel wff j ↾ 𝑡 k ∈ Comp
13 3 cv setvar x
14 13 9 cin class x ∩ k
15 14 10 wcel wff x ∩ k ∈ j ↾ 𝑡 k
16 12 15 wi wff j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k
17 16 7 6 wral wff ∀ k ∈ 𝒫 ⋃ j j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k
18 17 3 6 crab class x ∈ 𝒫 ⋃ j | ∀ k ∈ 𝒫 ⋃ j j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k
19 1 2 18 cmpt class j ∈ Top ⟼ x ∈ 𝒫 ⋃ j | ∀ k ∈ 𝒫 ⋃ j j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k
20 0 19 wceq wff 𝑘Gen = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j | ∀ k ∈ 𝒫 ⋃ j j ↾ 𝑡 k ∈ Comp → x ∩ k ∈ j ↾ 𝑡 k