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 ) ) } )

Metamath Proof Explorer

Definition df-kgen

Detailed syntax breakdown