Definition df-kgen 23908

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 23907	. 2 class 𝑘Gen
2		vj	. . 3 setvar 𝑗
3		ctop 23266	. . 3 class Top
4	2	cv 1569	. . . . . . . 8 class 𝑗
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1569	. . . . . . . 8 class 𝑘
7		crest 17641	. . . . . . . 8 class ↾t
8	4, 6, 7	co 7451	. . . . . . 7 class (𝑗 ↾t 𝑘)
9		ccmp 23759	. . . . . . 7 class Comp
10	8, 9	wcel 2147	. . . . . 6 wff (𝑗 ↾t 𝑘) ∈ Comp
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1569	. . . . . . . 8 class 𝑥
13	12, 6	cin 4092	. . . . . . 7 class (𝑥 ∩ 𝑘)
14	13, 8	wcel 2147	. . . . . 6 wff (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘)
15	10, 14	wi 4	. . . . 5 wff ((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))
16	4	cuni 4872	. . . . . 6 class ∪ 𝑗
17	16	cpw 4560	. . . . 5 class 𝒫 ∪ 𝑗
18	15, 5, 17	wral 3080	. . . 4 wff ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))
19	18, 11, 17	crab 3416	. . 3 class {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))}
20	2, 3, 19	cmpt 5192	. 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))})
21	1, 20	wceq 1570	1 wff 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))})

This definition is used by:  kgenval  23909  kgeni  23911  kgenf  23915