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 e. U. ran UnifOn |-> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` u ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctus
 |-  toUnifSp
1 vu
 |-  u
2 cust
 |-  UnifOn
3 2 crn
 |-  ran UnifOn
4 3 cuni
 |-  U. ran UnifOn
5 cbs
 |-  Base
6 cnx
 |-  ndx
7 6 5 cfv
 |-  ( Base ` ndx )
8 1 cv
 |-  u
9 8 cuni
 |-  U. u
10 9 cdm
 |-  dom U. u
11 7 10 cop
 |-  <. ( Base ` ndx ) , dom U. u >.
12 cunif
 |-  UnifSet
13 6 12 cfv
 |-  ( UnifSet ` ndx )
14 13 8 cop
 |-  <. ( UnifSet ` ndx ) , u >.
15 11 14 cpr
 |-  { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. }
16 csts
 |-  sSet
17 cts
 |-  TopSet
18 6 17 cfv
 |-  ( TopSet ` ndx )
19 cutop
 |-  unifTop
20 8 19 cfv
 |-  ( unifTop ` u )
21 18 20 cop
 |-  <. ( TopSet ` ndx ) , ( unifTop ` u ) >.
22 15 21 16 co
 |-  ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` u ) >. )
23 1 4 22 cmpt
 |-  ( u e. U. ran UnifOn |-> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` u ) >. ) )
24 0 23 wceq
 |-  toUnifSp = ( u e. U. ran UnifOn |-> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` u ) >. ) )