This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cusp

Description: Define the class of all complete uniform spaces. Definition 3 of BourbakiTop1 p. II.15. (Contributed by Thierry Arnoux, 1-Dec-2017)

Ref Expression
Assertion df-cusp 
|- CUnifSp = { w e. UnifSp | A. c e. ( Fil ` ( Base ` w ) ) ( c e. ( CauFilU ` ( UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccusp 
 |-  CUnifSp
1 vw 
 |-  w
2 cusp 
 |-  UnifSp
3 vc 
 |-  c
4 cfil 
 |-  Fil
5 cbs 
 |-  Base
6 1 cv 
 |-  w
7 6 5 cfv 
 |-  ( Base ` w )
8 7 4 cfv 
 |-  ( Fil ` ( Base ` w ) )
9 3 cv 
 |-  c
10 ccfilu 
 |-  CauFilU
11 cuss 
 |-  UnifSt
12 6 11 cfv 
 |-  ( UnifSt ` w )
13 12 10 cfv 
 |-  ( CauFilU ` ( UnifSt ` w ) )
14 9 13 wcel 
 |-  c e. ( CauFilU ` ( UnifSt ` w ) )
15 ctopn 
 |-  TopOpen
16 6 15 cfv 
 |-  ( TopOpen ` w )
17 cflim 
 |-  fLim
18 16 9 17 co 
 |-  ( ( TopOpen ` w ) fLim c )
19 c0 
 |-  (/)
20 18 19 wne 
 |-  ( ( TopOpen ` w ) fLim c ) =/= (/)
21 14 20 wi 
 |-  ( c e. ( CauFilU ` ( UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) )
22 21 3 8 wral 
 |-  A. c e. ( Fil ` ( Base ` w ) ) ( c e. ( CauFilU ` ( UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) )
23 22 1 2 crab 
 |-  { w e. UnifSp | A. c e. ( Fil ` ( Base ` w ) ) ( c e. ( CauFilU ` ( UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) }
24 0 23 wceq 
 |-  CUnifSp = { w e. UnifSp | A. c e. ( Fil ` ( Base ` w ) ) ( c e. ( CauFilU ` ( UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) }