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

Definition df-utop 22236
Description: Definition of a topology induced by a uniform structure. Definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
Assertion
Ref Expression
df-utop unifTop = (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
Distinct variable group:   𝑢,𝑎,𝑣,𝑥

Detailed syntax breakdown of Definition df-utop
StepHypRef Expression
1 cutop 22235 . 2 class unifTop
2 vu . . 3 setvar 𝑢
3 cust 22204 . . . . 5 class UnifOn
43crn 5267 . . . 4 class ran UnifOn
54cuni 4588 . . 3 class ran UnifOn
6 vv . . . . . . . . 9 setvar 𝑣
76cv 1631 . . . . . . . 8 class 𝑣
8 vx . . . . . . . . . 10 setvar 𝑥
98cv 1631 . . . . . . . . 9 class 𝑥
109csn 4321 . . . . . . . 8 class {𝑥}
117, 10cima 5269 . . . . . . 7 class (𝑣 “ {𝑥})
12 va . . . . . . . 8 setvar 𝑎
1312cv 1631 . . . . . . 7 class 𝑎
1411, 13wss 3715 . . . . . 6 wff (𝑣 “ {𝑥}) ⊆ 𝑎
152cv 1631 . . . . . 6 class 𝑢
1614, 6, 15wrex 3051 . . . . 5 wff 𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1716, 8, 13wral 3050 . . . 4 wff 𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1815cuni 4588 . . . . . 6 class 𝑢
1918cdm 5266 . . . . 5 class dom 𝑢
2019cpw 4302 . . . 4 class 𝒫 dom 𝑢
2117, 12, 20crab 3054 . . 3 class {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎}
222, 5, 21cmpt 4881 . 2 class (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
231, 22wceq 1632 1 wff unifTop = (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
Colors of variables: wff setvar class
This definition is referenced by:  utopval  22237
  Copyright terms: Public domain W3C validator