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 ) >. ) )