# Metamath Proof Explorer

## Definition df-utop

Description: Definition of a topology induced by a uniform structure. Definition 3 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017)

Ref Expression
Assertion df-utop ${⊢}\mathrm{unifTop}=\left({u}\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{{a}\in 𝒫\mathrm{dom}\bigcup {u}|\forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\exists {v}\in {u}\phantom{\rule{.4em}{0ex}}{v}\left[\left\{{x}\right\}\right]\subseteq {a}\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cutop ${class}\mathrm{unifTop}$
1 vu ${setvar}{u}$
2 cust ${class}\mathrm{UnifOn}$
3 2 crn ${class}\mathrm{ran}\mathrm{UnifOn}$
4 3 cuni ${class}\bigcup \mathrm{ran}\mathrm{UnifOn}$
5 va ${setvar}{a}$
6 1 cv ${setvar}{u}$
7 6 cuni ${class}\bigcup {u}$
8 7 cdm ${class}\mathrm{dom}\bigcup {u}$
9 8 cpw ${class}𝒫\mathrm{dom}\bigcup {u}$
10 vx ${setvar}{x}$
11 5 cv ${setvar}{a}$
12 vv ${setvar}{v}$
13 12 cv ${setvar}{v}$
14 10 cv ${setvar}{x}$
15 14 csn ${class}\left\{{x}\right\}$
16 13 15 cima ${class}{v}\left[\left\{{x}\right\}\right]$
17 16 11 wss ${wff}{v}\left[\left\{{x}\right\}\right]\subseteq {a}$
18 17 12 6 wrex ${wff}\exists {v}\in {u}\phantom{\rule{.4em}{0ex}}{v}\left[\left\{{x}\right\}\right]\subseteq {a}$
19 18 10 11 wral ${wff}\forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\exists {v}\in {u}\phantom{\rule{.4em}{0ex}}{v}\left[\left\{{x}\right\}\right]\subseteq {a}$
20 19 5 9 crab ${class}\left\{{a}\in 𝒫\mathrm{dom}\bigcup {u}|\forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\exists {v}\in {u}\phantom{\rule{.4em}{0ex}}{v}\left[\left\{{x}\right\}\right]\subseteq {a}\right\}$
21 1 4 20 cmpt ${class}\left({u}\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{{a}\in 𝒫\mathrm{dom}\bigcup {u}|\forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\exists {v}\in {u}\phantom{\rule{.4em}{0ex}}{v}\left[\left\{{x}\right\}\right]\subseteq {a}\right\}\right)$
22 0 21 wceq ${wff}\mathrm{unifTop}=\left({u}\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{{a}\in 𝒫\mathrm{dom}\bigcup {u}|\forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\exists {v}\in {u}\phantom{\rule{.4em}{0ex}}{v}\left[\left\{{x}\right\}\right]\subseteq {a}\right\}\right)$