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 23381
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 23380 . 2 class unifTop
2 vu . . 3 setvar 𝑢
3 cust 23349 . . . . 5 class UnifOn
43crn 5592 . . . 4 class ran UnifOn
54cuni 4841 . . 3 class ran UnifOn
6 vv . . . . . . . . 9 setvar 𝑣
76cv 1538 . . . . . . . 8 class 𝑣
8 vx . . . . . . . . . 10 setvar 𝑥
98cv 1538 . . . . . . . . 9 class 𝑥
109csn 4563 . . . . . . . 8 class {𝑥}
117, 10cima 5594 . . . . . . 7 class (𝑣 “ {𝑥})
12 va . . . . . . . 8 setvar 𝑎
1312cv 1538 . . . . . . 7 class 𝑎
1411, 13wss 3888 . . . . . 6 wff (𝑣 “ {𝑥}) ⊆ 𝑎
152cv 1538 . . . . . 6 class 𝑢
1614, 6, 15wrex 3065 . . . . 5 wff 𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1716, 8, 13wral 3064 . . . 4 wff 𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1815cuni 4841 . . . . . 6 class 𝑢
1918cdm 5591 . . . . 5 class dom 𝑢
2019cpw 4535 . . . 4 class 𝒫 dom 𝑢
2117, 12, 20crab 3068 . . 3 class {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎}
222, 5, 21cmpt 5159 . 2 class (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
231, 22wceq 1539 1 wff unifTop = (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
Colors of variables: wff setvar class
This definition is referenced by:  utopval  23382
  Copyright terms: Public domain W3C validator