Definition df-ust 22004

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

Assertion

Ref	Expression
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 ) ) ) } )

Distinct variable group:   x, u, v, w

Detailed syntax breakdown of Definition df-ust

Step	Hyp	Ref	Expression
1		cust 22003	. 2 class UnifOn
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vu	. . . . . . 7 setvar u
5	4	cv 1482	. . . . . 6 class u
6	2	cv 1482	. . . . . . . 8 class x
7	6, 6	cxp 5112	. . . . . . 7 class ( x X. x )
8	7	cpw 4158	. . . . . 6 class ~P ( x X. x )
9	5, 8	wss 3574	. . . . 5 wff u C_ ~P ( x X. x )
10	7, 5	wcel 1990	. . . . 5 wff ( x X. x ) e. u
11		vv	. . . . . . . . . . 11 setvar v
12	11	cv 1482	. . . . . . . . . 10 class v
13		vw	. . . . . . . . . . 11 setvar w
14	13	cv 1482	. . . . . . . . . 10 class w
15	12, 14	wss 3574	. . . . . . . . 9 wff v C_ w
16	13, 4	wel 1991	. . . . . . . . 9 wff w e. u
17	15, 16	wi 4	. . . . . . . 8 wff ( v C_ w -> w e. u )
18	17, 13, 8	wral 2912	. . . . . . 7 wff A. w e. ~P ( x X. x ) ( v C_ w -> w e. u )
19	12, 14	cin 3573	. . . . . . . . 9 class ( v i^i w )
20	19, 5	wcel 1990	. . . . . . . 8 wff ( v i^i w ) e. u
21	20, 13, 5	wral 2912	. . . . . . 7 wff A. w e. u ( v i^i w ) e. u
22		cid 5023	. . . . . . . . . 10 class _I
23	22, 6	cres 5116	. . . . . . . . 9 class ( _I |` x )
24	23, 12	wss 3574	. . . . . . . 8 wff ( _I |` x ) C_ v
25	12	ccnv 5113	. . . . . . . . 9 class `' v
26	25, 5	wcel 1990	. . . . . . . 8 wff `' v e. u
27	14, 14	ccom 5118	. . . . . . . . . 10 class ( w o. w )
28	27, 12	wss 3574	. . . . . . . . 9 wff ( w o. w ) C_ v
29	28, 13, 5	wrex 2913	. . . . . . . 8 wff E. w e. u ( w o. w ) C_ v
30	24, 26, 29	w3a 1037	. . . . . . 7 wff ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v )
31	18, 21, 30	w3a 1037	. . . . . 6 wff ( 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	31, 11, 5	wral 2912	. . . . 5 wff 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	9, 10, 32	w3a 1037	. . . 4 wff ( 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	33, 4	cab 2608	. . 3 class { 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	2, 3, 34	cmpt 4729	. 2 class ( 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 ) ) ) } )
36	1, 35	wceq 1483	1 wff 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 ) ) ) } )

This definition is referenced by:  ustfn  22005  ustval  22006  ustn0  22024