Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-kgen Structured version   Visualization version   GIF version

Definition df-kgen 21147
 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
StepHypRef Expression
1 ckgen 21146 . 2 class 𝑘Gen
2 vj . . 3 setvar 𝑗
3 ctop 20517 . . 3 class Top
42cv 1474 . . . . . . . 8 class 𝑗
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1474 . . . . . . . 8 class 𝑘
7 crest 15904 . . . . . . . 8 class t
84, 6, 7co 6549 . . . . . . 7 class (𝑗t 𝑘)
9 ccmp 20999 . . . . . . 7 class Comp
108, 9wcel 1977 . . . . . 6 wff (𝑗t 𝑘) ∈ Comp
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1474 . . . . . . . 8 class 𝑥
1312, 6cin 3539 . . . . . . 7 class (𝑥𝑘)
1413, 8wcel 1977 . . . . . 6 wff (𝑥𝑘) ∈ (𝑗t 𝑘)
1510, 14wi 4 . . . . 5 wff ((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
164cuni 4372 . . . . . 6 class 𝑗
1716cpw 4108 . . . . 5 class 𝒫 𝑗
1815, 5, 17wral 2896 . . . 4 wff 𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
1918, 11, 17crab 2900 . . 3 class {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))}
202, 3, 19cmpt 4643 . 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
211, 20wceq 1475 1 wff 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
 Colors of variables: wff setvar class This definition is referenced by:  kgenval  21148  kgeni  21150  kgenf  21154
 Copyright terms: Public domain W3C validator