Definition df-kgen 23542

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 23541	. 2 class 𝑘Gen
2		vj	. . 3 setvar 𝑗
3		ctop 22899	. . 3 class Top
4	2	cv 1539	. . . . . . . 8 class 𝑗
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1539	. . . . . . . 8 class 𝑘
7		crest 17465	. . . . . . . 8 class ↾t
8	4, 6, 7	co 7431	. . . . . . 7 class (𝑗 ↾t 𝑘)
9		ccmp 23394	. . . . . . 7 class Comp
10	8, 9	wcel 2108	. . . . . 6 wff (𝑗 ↾t 𝑘) ∈ Comp
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1539	. . . . . . . 8 class 𝑥
13	12, 6	cin 3950	. . . . . . 7 class (𝑥 ∩ 𝑘)
14	13, 8	wcel 2108	. . . . . 6 wff (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘)
15	10, 14	wi 4	. . . . 5 wff ((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))
16	4	cuni 4907	. . . . . 6 class ∪ 𝑗
17	16	cpw 4600	. . . . 5 class 𝒫 ∪ 𝑗
18	15, 5, 17	wral 3061	. . . 4 wff ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))
19	18, 11, 17	crab 3436	. . 3 class {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))}
20	2, 3, 19	cmpt 5225	. 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))})
21	1, 20	wceq 1540	1 wff 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))})

This definition is referenced by:  kgenval  23543  kgeni  23545  kgenf  23549