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

Definition df-utop 22835
 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 22834 . 2 class unifTop
2 vu . . 3 setvar 𝑢
3 cust 22803 . . . . 5 class UnifOn
43crn 5533 . . . 4 class ran UnifOn
54cuni 4813 . . 3 class ran UnifOn
6 vv . . . . . . . . 9 setvar 𝑣
76cv 1537 . . . . . . . 8 class 𝑣
8 vx . . . . . . . . . 10 setvar 𝑥
98cv 1537 . . . . . . . . 9 class 𝑥
109csn 4539 . . . . . . . 8 class {𝑥}
117, 10cima 5535 . . . . . . 7 class (𝑣 “ {𝑥})
12 va . . . . . . . 8 setvar 𝑎
1312cv 1537 . . . . . . 7 class 𝑎
1411, 13wss 3908 . . . . . 6 wff (𝑣 “ {𝑥}) ⊆ 𝑎
152cv 1537 . . . . . 6 class 𝑢
1614, 6, 15wrex 3131 . . . . 5 wff 𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1716, 8, 13wral 3130 . . . 4 wff 𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1815cuni 4813 . . . . . 6 class 𝑢
1918cdm 5532 . . . . 5 class dom 𝑢
2019cpw 4511 . . . 4 class 𝒫 dom 𝑢
2117, 12, 20crab 3134 . . 3 class {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎}
222, 5, 21cmpt 5122 . 2 class (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
231, 22wceq 1538 1 wff unifTop = (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
 Colors of variables: wff setvar class This definition is referenced by:  utopval  22836
 Copyright terms: Public domain W3C validator