Metamath Proof Explorer


Definition df-tus

Description: Define the function mapping a uniform structure to a uniform space. (Contributed by Thierry Arnoux, 17-Nov-2017)

Ref Expression
Assertion df-tus toUnifSp = u ran UnifOn Base ndx dom u UnifSet ndx u sSet TopSet ndx unifTop u

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctus class toUnifSp
1 vu setvar u
2 cust class UnifOn
3 2 crn class ran UnifOn
4 3 cuni class ran UnifOn
5 cbs class Base
6 cnx class ndx
7 6 5 cfv class Base ndx
8 1 cv setvar u
9 8 cuni class u
10 9 cdm class dom u
11 7 10 cop class Base ndx dom u
12 cunif class UnifSet
13 6 12 cfv class UnifSet ndx
14 13 8 cop class UnifSet ndx u
15 11 14 cpr class Base ndx dom u UnifSet ndx u
16 csts class sSet
17 cts class TopSet
18 6 17 cfv class TopSet ndx
19 cutop class unifTop
20 8 19 cfv class unifTop u
21 18 20 cop class TopSet ndx unifTop u
22 15 21 16 co class Base ndx dom u UnifSet ndx u sSet TopSet ndx unifTop u
23 1 4 22 cmpt class u ran UnifOn Base ndx dom u UnifSet ndx u sSet TopSet ndx unifTop u
24 0 23 wceq wff toUnifSp = u ran UnifOn Base ndx dom u UnifSet ndx u sSet TopSet ndx unifTop u