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 21385
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 21384 . 2 class 𝑘Gen
2 vj . . 3 setvar 𝑗
3 ctop 20746 . . 3 class Top
42cv 1522 . . . . . . . 8 class 𝑗
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1522 . . . . . . . 8 class 𝑘
7 crest 16128 . . . . . . . 8 class t
84, 6, 7co 6690 . . . . . . 7 class (𝑗t 𝑘)
9 ccmp 21237 . . . . . . 7 class Comp
108, 9wcel 2030 . . . . . 6 wff (𝑗t 𝑘) ∈ Comp
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1522 . . . . . . . 8 class 𝑥
1312, 6cin 3606 . . . . . . 7 class (𝑥𝑘)
1413, 8wcel 2030 . . . . . 6 wff (𝑥𝑘) ∈ (𝑗t 𝑘)
1510, 14wi 4 . . . . 5 wff ((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
164cuni 4468 . . . . . 6 class 𝑗
1716cpw 4191 . . . . 5 class 𝒫 𝑗
1815, 5, 17wral 2941 . . . 4 wff 𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
1918, 11, 17crab 2945 . . 3 class {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))}
202, 3, 19cmpt 4762 . 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
211, 20wceq 1523 1 wff 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
Colors of variables: wff setvar class
This definition is referenced by:  kgenval  21386  kgeni  21388  kgenf  21392
  Copyright terms: Public domain W3C validator