Definition df-kgen 21337

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

Assertion

Ref	Expression
df-kgen	|- 𝑘Gen = ( j e. Top |-> { x e. ~P U. j | A. k e. ~P U. j ( ( j ↾t k ) e. Comp -> ( x i^i k ) e. ( j ↾t k ) ) } )

Distinct variable group:   j, k, x

Detailed syntax breakdown of Definition df-kgen

Step	Hyp	Ref	Expression
1		ckgen 21336	. 2 class 𝑘Gen
2		vj	. . 3 setvar j
3		ctop 20698	. . 3 class Top
4	2	cv 1482	. . . . . . . 8 class j
5		vk	. . . . . . . . 9 setvar k
6	5	cv 1482	. . . . . . . 8 class k
7		crest 16081	. . . . . . . 8 class ↾t
8	4, 6, 7	co 6650	. . . . . . 7 class ( j ↾t k )
9		ccmp 21189	. . . . . . 7 class Comp
10	8, 9	wcel 1990	. . . . . 6 wff ( j ↾t k ) e. Comp
11		vx	. . . . . . . . 9 setvar x
12	11	cv 1482	. . . . . . . 8 class x
13	12, 6	cin 3573	. . . . . . 7 class ( x i^i k )
14	13, 8	wcel 1990	. . . . . 6 wff ( x i^i k ) e. ( j ↾t k )
15	10, 14	wi 4	. . . . 5 wff ( ( j ↾t k ) e. Comp -> ( x i^i k ) e. ( j ↾t k ) )
16	4	cuni 4436	. . . . . 6 class U. j
17	16	cpw 4158	. . . . 5 class ~P U. j
18	15, 5, 17	wral 2912	. . . 4 wff A. k e. ~P U. j ( ( j ↾t k ) e. Comp -> ( x i^i k ) e. ( j ↾t k ) )
19	18, 11, 17	crab 2916	. . 3 class { x e. ~P U. j | A. k e. ~P U. j ( ( j ↾t k ) e. Comp -> ( x i^i k ) e. ( j ↾t k ) ) }
20	2, 3, 19	cmpt 4729	. 2 class ( j e. Top |-> { x e. ~P U. j | A. k e. ~P U. j ( ( j ↾t k ) e. Comp -> ( x i^i k ) e. ( j ↾t k ) ) } )
21	1, 20	wceq 1483	1 wff 𝑘Gen = ( j e. Top |-> { x e. ~P U. j | A. k e. ~P U. j ( ( j ↾t k ) e. Comp -> ( x i^i k ) e. ( j ↾t k ) ) } )

This definition is referenced by:  kgenval  21338  kgeni  21340  kgenf  21344