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 22683
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 22682 . 2 class 𝑘Gen
2 vj . . 3 setvar 𝑗
3 ctop 22040 . . 3 class Top
42cv 1541 . . . . . . . 8 class 𝑗
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1541 . . . . . . . 8 class 𝑘
7 crest 17129 . . . . . . . 8 class t
84, 6, 7co 7271 . . . . . . 7 class (𝑗t 𝑘)
9 ccmp 22535 . . . . . . 7 class Comp
108, 9wcel 2110 . . . . . 6 wff (𝑗t 𝑘) ∈ Comp
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1541 . . . . . . . 8 class 𝑥
1312, 6cin 3891 . . . . . . 7 class (𝑥𝑘)
1413, 8wcel 2110 . . . . . 6 wff (𝑥𝑘) ∈ (𝑗t 𝑘)
1510, 14wi 4 . . . . 5 wff ((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
164cuni 4845 . . . . . 6 class 𝑗
1716cpw 4539 . . . . 5 class 𝒫 𝑗
1815, 5, 17wral 3066 . . . 4 wff 𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
1918, 11, 17crab 3070 . . 3 class {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))}
202, 3, 19cmpt 5162 . 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
211, 20wceq 1542 1 wff 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
Colors of variables: wff setvar class
This definition is referenced by:  kgenval  22684  kgeni  22686  kgenf  22690
  Copyright terms: Public domain W3C validator