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 22070
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 22069 . 2 class 𝑘Gen
2 vj . . 3 setvar 𝑗
3 ctop 21429 . . 3 class Top
42cv 1527 . . . . . . . 8 class 𝑗
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1527 . . . . . . . 8 class 𝑘
7 crest 16682 . . . . . . . 8 class t
84, 6, 7co 7145 . . . . . . 7 class (𝑗t 𝑘)
9 ccmp 21922 . . . . . . 7 class Comp
108, 9wcel 2105 . . . . . 6 wff (𝑗t 𝑘) ∈ Comp
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1527 . . . . . . . 8 class 𝑥
1312, 6cin 3932 . . . . . . 7 class (𝑥𝑘)
1413, 8wcel 2105 . . . . . 6 wff (𝑥𝑘) ∈ (𝑗t 𝑘)
1510, 14wi 4 . . . . 5 wff ((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
164cuni 4830 . . . . . 6 class 𝑗
1716cpw 4535 . . . . 5 class 𝒫 𝑗
1815, 5, 17wral 3135 . . . 4 wff 𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))
1918, 11, 17crab 3139 . . 3 class {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))}
202, 3, 19cmpt 5137 . 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
211, 20wceq 1528 1 wff 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ∀𝑘 ∈ 𝒫 𝑗((𝑗t 𝑘) ∈ Comp → (𝑥𝑘) ∈ (𝑗t 𝑘))})
Colors of variables: wff setvar class
This definition is referenced by:  kgenval  22071  kgeni  22073  kgenf  22077
  Copyright terms: Public domain W3C validator