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 22082
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 22081 . 2 class unifTop
2 vu . . 3 setvar 𝑢
3 cust 22050 . . . . 5 class UnifOn
43crn 5144 . . . 4 class ran UnifOn
54cuni 4468 . . 3 class ran UnifOn
6 vv . . . . . . . . 9 setvar 𝑣
76cv 1522 . . . . . . . 8 class 𝑣
8 vx . . . . . . . . . 10 setvar 𝑥
98cv 1522 . . . . . . . . 9 class 𝑥
109csn 4210 . . . . . . . 8 class {𝑥}
117, 10cima 5146 . . . . . . 7 class (𝑣 “ {𝑥})
12 va . . . . . . . 8 setvar 𝑎
1312cv 1522 . . . . . . 7 class 𝑎
1411, 13wss 3607 . . . . . 6 wff (𝑣 “ {𝑥}) ⊆ 𝑎
152cv 1522 . . . . . 6 class 𝑢
1614, 6, 15wrex 2942 . . . . 5 wff 𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1716, 8, 13wral 2941 . . . 4 wff 𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1815cuni 4468 . . . . . 6 class 𝑢
1918cdm 5143 . . . . 5 class dom 𝑢
2019cpw 4191 . . . 4 class 𝒫 dom 𝑢
2117, 12, 20crab 2945 . . 3 class {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎}
222, 5, 21cmpt 4762 . 2 class (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
231, 22wceq 1523 1 wff unifTop = (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
Colors of variables: wff setvar class
This definition is referenced by:  utopval  22083
  Copyright terms: Public domain W3C validator