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

Definition df-topgen 16312
Description: Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78 (see tgval2 20978). The first use of this definition is tgval 20977 but the token is used in df-pt 16313. See tgval3 20985 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.)
Assertion
Ref Expression
df-topgen topGen = (𝑥 ∈ V ↦ {𝑦𝑦 (𝑥 ∩ 𝒫 𝑦)})
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-topgen
StepHypRef Expression
1 ctg 16306 . 2 class topGen
2 vx . . 3 setvar 𝑥
3 cvv 3398 . . 3 class V
4 vy . . . . . 6 setvar 𝑦
54cv 1636 . . . . 5 class 𝑦
62cv 1636 . . . . . . 7 class 𝑥
75cpw 4358 . . . . . . 7 class 𝒫 𝑦
86, 7cin 3775 . . . . . 6 class (𝑥 ∩ 𝒫 𝑦)
98cuni 4637 . . . . 5 class (𝑥 ∩ 𝒫 𝑦)
105, 9wss 3776 . . . 4 wff 𝑦 (𝑥 ∩ 𝒫 𝑦)
1110, 4cab 2799 . . 3 class {𝑦𝑦 (𝑥 ∩ 𝒫 𝑦)}
122, 3, 11cmpt 4930 . 2 class (𝑥 ∈ V ↦ {𝑦𝑦 (𝑥 ∩ 𝒫 𝑦)})
131, 12wceq 1637 1 wff topGen = (𝑥 ∈ V ↦ {𝑦𝑦 (𝑥 ∩ 𝒫 𝑦)})
Colors of variables: wff setvar class
This definition is referenced by:  tgval  20977
  Copyright terms: Public domain W3C validator