Definition df-utop

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cutop	|- unifTop
1		vu	|- u
2		cust	|- UnifOn
3	2	crn	|- ran UnifOn
4	3	cuni	|- U. ran UnifOn
5		va	|- a
6	1	cv	|- u
7	6	cuni	|- U. u
8	7	cdm	|- dom U. u
9	8	cpw	|- ~P dom U. u
10		vx	|- x
11	5	cv	|- a
12		vv	|- v
13	12	cv	|- v
14	10	cv	|- x
15	14	csn	|- { x }
16	13 15	cima	|- ( v " { x } )
17	16 11	wss	|- ( v " { x } ) C_ a
18	17 12 6	wrex	|- E. v e. u ( v " { x } ) C_ a
19	18 10 11	wral	|- A. x e. a E. v e. u ( v " { x } ) C_ a
20	19 5 9	crab	|- { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a }
21	1 4 20	cmpt	|- ( u e. U. ran UnifOn |-> { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a } )
22	0 21	wceq	|- unifTop = ( u e. U. ran UnifOn |-> { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a } )