Metamath Proof Explorer

Definition df-ust

Description: Definition of a uniform structure. Definition 1 of BourbakiTop1 p. II.1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. This definition is analogous to TopOn . Elements of an uniform structure are called entourages. (Contributed by FL, 29-May-2014) (Revised by Thierry Arnoux, 15-Nov-2017)

Ref Expression
Assertion df-ust 
|- UnifOn = ( x e. _V |-> { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cust 
 |-  UnifOn
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vu 
 |-  u
4 3 cv 
 |-  u
5 1 cv 
 |-  x
6 5 5 cxp 
 |-  ( x X. x )
7 6 cpw 
 |-  ~P ( x X. x )
8 4 7 wss 
 |-  u C_ ~P ( x X. x )
9 6 4 wcel 
 |-  ( x X. x ) e. u
10 vv 
 |-  v
11 vw 
 |-  w
12 10 cv 
 |-  v
13 11 cv 
 |-  w
14 12 13 wss 
 |-  v C_ w
15 13 4 wcel 
 |-  w e. u
16 14 15 wi 
 |-  ( v C_ w -> w e. u )
17 16 11 7 wral 
 |-  A. w e. ~P ( x X. x ) ( v C_ w -> w e. u )
18 12 13 cin 
 |-  ( v i^i w )
19 18 4 wcel 
 |-  ( v i^i w ) e. u
20 19 11 4 wral 
 |-  A. w e. u ( v i^i w ) e. u
21 cid 
 |-  _I
22 21 5 cres 
 |-  ( _I |` x )
23 22 12 wss 
 |-  ( _I |` x ) C_ v
24 12 ccnv 
 |-  `' v
25 24 4 wcel 
 |-  `' v e. u
26 13 13 ccom 
 |-  ( w o. w )
27 26 12 wss 
 |-  ( w o. w ) C_ v
28 27 11 4 wrex 
 |-  E. w e. u ( w o. w ) C_ v
29 23 25 28 w3a 
 |-  ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v )
30 17 20 29 w3a 
 |-  ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) )
31 30 10 4 wral 
 |-  A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) )
32 8 9 31 w3a 
 |-  ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) )
33 32 3 cab 
 |-  { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) }
34 1 2 33 cmpt 
 |-  ( x e. _V |-> { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } )
35 0 34 wceq 
 |-  UnifOn = ( x e. _V |-> { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } )