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	$⊢ 𝑘Gen = (j \in Top ⟼ \{x \in 𝒫 ⋃ j \| \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ckgen	$class 𝑘Gen$
1		vj	$setvar j$
2		ctop	$class Top$
3		vx	$setvar x$
4	1	cv	$setvar j$
5	4	cuni	$class ⋃ j$
6	5	cpw	$class 𝒫 ⋃ j$
7		vk	$setvar k$
8		crest	$class ↾_{𝑡}$
9	7	cv	$setvar k$
10	4 9 8	co	$class (j ↾_{𝑡} k)$
11		ccmp	$class Comp$
12	10 11	wcel	$wff j ↾_{𝑡} k \in Comp$
13	3	cv	$setvar x$
14	13 9	cin	$class (x \cap k)$
15	14 10	wcel	$wff x \cap k \in (j ↾_{𝑡} k)$
16	12 15	wi	$wff (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))$
17	16 7 6	wral	$wff \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))$
18	17 3 6	crab	$class \{x \in 𝒫 ⋃ j \| \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))\}$
19	1 2 18	cmpt	$class (j \in Top ⟼ \{x \in 𝒫 ⋃ j \| \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))\})$
20	0 19	wceq	$wff 𝑘Gen = (j \in Top ⟼ \{x \in 𝒫 ⋃ j \| \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))\})$

Metamath Proof Explorer

Definition df-kgen

Detailed syntax breakdown