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 unifTop=uranUnifOna𝒫domu|xavuvxa

Detailed syntax breakdown

Step Hyp Ref Expression
0 cutop classunifTop
1 vu setvaru
2 cust classUnifOn
3 2 crn classranUnifOn
4 3 cuni classranUnifOn
5 va setvara
6 1 cv setvaru
7 6 cuni classu
8 7 cdm classdomu
9 8 cpw class𝒫domu
10 vx setvarx
11 5 cv setvara
12 vv setvarv
13 12 cv setvarv
14 10 cv setvarx
15 14 csn classx
16 13 15 cima classvx
17 16 11 wss wffvxa
18 17 12 6 wrex wffvuvxa
19 18 10 11 wral wffxavuvxa
20 19 5 9 crab classa𝒫domu|xavuvxa
21 1 4 20 cmpt classuranUnifOna𝒫domu|xavuvxa
22 0 21 wceq wffunifTop=uranUnifOna𝒫domu|xavuvxa