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 21793
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 21792 . 2 class unifTop
2 vu . . 3 setvar 𝑢
3 cust 21761 . . . . 5 class UnifOn
43crn 5029 . . . 4 class ran UnifOn
54cuni 4366 . . 3 class ran UnifOn
6 vv . . . . . . . . 9 setvar 𝑣
76cv 1473 . . . . . . . 8 class 𝑣
8 vx . . . . . . . . . 10 setvar 𝑥
98cv 1473 . . . . . . . . 9 class 𝑥
109csn 4124 . . . . . . . 8 class {𝑥}
117, 10cima 5031 . . . . . . 7 class (𝑣 “ {𝑥})
12 va . . . . . . . 8 setvar 𝑎
1312cv 1473 . . . . . . 7 class 𝑎
1411, 13wss 3539 . . . . . 6 wff (𝑣 “ {𝑥}) ⊆ 𝑎
152cv 1473 . . . . . 6 class 𝑢
1614, 6, 15wrex 2896 . . . . 5 wff 𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1716, 8, 13wral 2895 . . . 4 wff 𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
1815cuni 4366 . . . . . 6 class 𝑢
1918cdm 5028 . . . . 5 class dom 𝑢
2019cpw 4107 . . . 4 class 𝒫 dom 𝑢
2117, 12, 20crab 2899 . . 3 class {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎}
222, 5, 21cmpt 4637 . 2 class (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
231, 22wceq 1474 1 wff unifTop = (𝑢 ran UnifOn ↦ {𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀𝑥𝑎𝑣𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
Colors of variables: wff setvar class
This definition is referenced by:  utopval  21794
  Copyright terms: Public domain W3C validator