Definition df-kgen 22593

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. 𝑥 ∈ (𝑘Gen‘𝑗), iff the preimage of 𝑥 is open in all compact Hausdorff spaces. (Contributed by Mario Carneiro, 20-Mar-2015.)

Assertion

Ref	Expression
df-kgen	⊢ 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))})

Distinct variable group:   𝑗,𝑘,𝑥

Detailed syntax breakdown of Definition df-kgen

Step	Hyp	Ref	Expression
1		ckgen 22592	. 2 class 𝑘Gen
2		vj	. . 3 setvar 𝑗
3		ctop 21950	. . 3 class Top
4	2	cv 1538	. . . . . . . 8 class 𝑗
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1538	. . . . . . . 8 class 𝑘
7		crest 17048	. . . . . . . 8 class ↾t
8	4, 6, 7	co 7255	. . . . . . 7 class (𝑗 ↾t 𝑘)
9		ccmp 22445	. . . . . . 7 class Comp
10	8, 9	wcel 2108	. . . . . 6 wff (𝑗 ↾t 𝑘) ∈ Comp
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1538	. . . . . . . 8 class 𝑥
13	12, 6	cin 3882	. . . . . . 7 class (𝑥 ∩ 𝑘)
14	13, 8	wcel 2108	. . . . . 6 wff (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘)
15	10, 14	wi 4	. . . . 5 wff ((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))
16	4	cuni 4836	. . . . . 6 class ∪ 𝑗
17	16	cpw 4530	. . . . 5 class 𝒫 ∪ 𝑗
18	15, 5, 17	wral 3063	. . . 4 wff ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))
19	18, 11, 17	crab 3067	. . 3 class {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))}
20	2, 3, 19	cmpt 5153	. 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))})
21	1, 20	wceq 1539	1 wff 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))})

This definition is referenced by:  kgenval  22594  kgeni  22596  kgenf  22600