Definition df-utop 22035

Description: Definition of a topology induced by a uniform structure. Definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)

Assertion

Ref	Expression
df-utop	|- unifTop = ( u e. U. ran UnifOn |-> { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a } )

Distinct variable group:   u, a, v, x

Detailed syntax breakdown of Definition df-utop

Step	Hyp	Ref	Expression
1		cutop 22034	. 2 class unifTop
2		vu	. . 3 setvar u
3		cust 22003	. . . . 5 class UnifOn
4	3	crn 5115	. . . 4 class ran UnifOn
5	4	cuni 4436	. . 3 class U. ran UnifOn
6		vv	. . . . . . . . 9 setvar v
7	6	cv 1482	. . . . . . . 8 class v
8		vx	. . . . . . . . . 10 setvar x
9	8	cv 1482	. . . . . . . . 9 class x
10	9	csn 4177	. . . . . . . 8 class { x }
11	7, 10	cima 5117	. . . . . . 7 class ( v " { x } )
12		va	. . . . . . . 8 setvar a
13	12	cv 1482	. . . . . . 7 class a
14	11, 13	wss 3574	. . . . . 6 wff ( v " { x } ) C_ a
15	2	cv 1482	. . . . . 6 class u
16	14, 6, 15	wrex 2913	. . . . 5 wff E. v e. u ( v " { x } ) C_ a
17	16, 8, 13	wral 2912	. . . 4 wff A. x e. a E. v e. u ( v " { x } ) C_ a
18	15	cuni 4436	. . . . . 6 class U. u
19	18	cdm 5114	. . . . 5 class dom U. u
20	19	cpw 4158	. . . 4 class ~P dom U. u
21	17, 12, 20	crab 2916	. . 3 class { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a }
22	2, 5, 21	cmpt 4729	. 2 class ( u e. U. ran UnifOn |-> { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a } )
23	1, 22	wceq 1483	1 wff unifTop = ( u e. U. ran UnifOn |-> { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a } )

This definition is referenced by:  utopval  22036