Metamath Proof Explorer

Definition df-usp

Description: Definition of a uniform space, i.e. a base set with an uniform structure and its induced topology. Derived from definition 3 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017)

Ref Expression
Assertion df-usp 
|- UnifSp = { f | ( ( UnifSt ` f ) e. ( UnifOn ` ( Base ` f ) ) /\ ( TopOpen ` f ) = ( unifTop ` ( UnifSt ` f ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cusp 
 |-  UnifSp
1 vf 
 |-  f
2 cuss 
 |-  UnifSt
3 1 cv 
 |-  f
4 3 2 cfv 
 |-  ( UnifSt ` f )
5 cust 
 |-  UnifOn
6 cbs 
 |-  Base
7 3 6 cfv 
 |-  ( Base ` f )
8 7 5 cfv 
 |-  ( UnifOn ` ( Base ` f ) )
9 4 8 wcel 
 |-  ( UnifSt ` f ) e. ( UnifOn ` ( Base ` f ) )
10 ctopn 
 |-  TopOpen
11 3 10 cfv 
 |-  ( TopOpen ` f )
12 cutop 
 |-  unifTop
13 4 12 cfv 
 |-  ( unifTop ` ( UnifSt ` f ) )
14 11 13 wceq 
 |-  ( TopOpen ` f ) = ( unifTop ` ( UnifSt ` f ) )
15 9 14 wa 
 |-  ( ( UnifSt ` f ) e. ( UnifOn ` ( Base ` f ) ) /\ ( TopOpen ` f ) = ( unifTop ` ( UnifSt ` f ) ) )
16 15 1 cab 
 |-  { f | ( ( UnifSt ` f ) e. ( UnifOn ` ( Base ` f ) ) /\ ( TopOpen ` f ) = ( unifTop ` ( UnifSt ` f ) ) ) }
17 0 16 wceq 
 |-  UnifSp = { f | ( ( UnifSt ` f ) e. ( UnifOn ` ( Base ` f ) ) /\ ( TopOpen ` f ) = ( unifTop ` ( UnifSt ` f ) ) ) }