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

Definition df-kgen 21089
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 21088 . 2 class 𝑘Gen
2 vj . . 3 setvar 𝑗
3 ctop 20459 . . 3 class Top
42cv 1473 . . . . . . . 8 class 𝑗
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1473 . . . . . . . 8 class 𝑘
7 crest 15850 . . . . . . . 8 class t
84, 6, 7co 6527 . . . . . . 7 class (𝑗t 𝑘)
9 ccmp 20941 . . . . . . 7 class Comp
108, 9wcel 1976 . . . . . 6 wff (𝑗t 𝑘) ∈ Comp
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1473 . . . . . . . 8 class 𝑥
1312, 6cin 3538 . . . . . . 7 class (𝑥𝑘)
1413, 8wcel 1976 . . . . . 6 wff (𝑥𝑘) ∈ (𝑗t 𝑘)
1510, 14wi 4 . . . . 5 wff ((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
164cuni 4366 . . . . . 6 class 𝑗
1716cpw 4107 . . . . 5 class 𝒫 𝑗
1815, 5, 17wral 2895 . . . 4 wff 𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
1918, 11, 17crab 2899 . . 3 class {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))}
202, 3, 19cmpt 4637 . 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
211, 20wceq 1474 1 wff 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
Colors of variables: wff setvar class
This definition is referenced by:  kgenval  21090  kgeni  21092  kgenf  21096
  Copyright terms: Public domain W3C validator