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	|- kGen = ( 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 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ckgen	|- kGen
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5	4	cuni	|- U. j
6	5	cpw	|- ~P U. j
7		vk	|- k
8		crest	|- |`t
9	7	cv	|- k
10	4 9 8	co	|- ( j |`t k )
11		ccmp	|- Comp
12	10 11	wcel	|- ( j |`t k ) e. Comp
13	3	cv	|- x
14	13 9	cin	|- ( x i^i k )
15	14 10	wcel	|- ( x i^i k ) e. ( j |`t k )
16	12 15	wi	|- ( ( j |`t k ) e. Comp -> ( x i^i k ) e. ( j |`t k ) )
17	16 7 6	wral	|- A. k e. ~P U. j ( ( j |`t k ) e. Comp -> ( x i^i k ) e. ( j |`t k ) )
18	17 3 6	crab	|- { x e. ~P U. j | A. k e. ~P U. j ( ( j |`t k ) e. Comp -> ( x i^i k ) e. ( j |`t k ) ) }
19	1 2 18	cmpt	|- ( 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 ) ) } )
20	0 19	wceq	|- kGen = ( 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 ) ) } )