Theorem elutop

Description: Open sets in the topology induced by an uniform structure U on X (Contributed by Thierry Arnoux, 30-Nov-2017)

	Ref	Expression
Assertion	elutop	|- ( U e. ( UnifOn ` X ) -> ( A e. ( unifTop ` U ) <-> ( A C_ X /\ A. x e. A E. v e. U ( v " { x } ) C_ A ) ) )

Proof

Step	Hyp	Ref	Expression
1		utopval	|- ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } )
2	1	eleq2d	|- ( U e. ( UnifOn ` X ) -> ( A e. ( unifTop ` U ) <-> A e. { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } ) )
3		sseq2	|- ( a = A -> ( ( v " { x } ) C_ a <-> ( v " { x } ) C_ A ) )
4	3	rexbidv	|- ( a = A -> ( E. v e. U ( v " { x } ) C_ a <-> E. v e. U ( v " { x } ) C_ A ) )
5	4	raleqbi1dv	|- ( a = A -> ( A. x e. a E. v e. U ( v " { x } ) C_ a <-> A. x e. A E. v e. U ( v " { x } ) C_ A ) )
6	5	elrab	|- ( A e. { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } <-> ( A e. ~P X /\ A. x e. A E. v e. U ( v " { x } ) C_ A ) )
7	2 6	bitrdi	|- ( U e. ( UnifOn ` X ) -> ( A e. ( unifTop ` U ) <-> ( A e. ~P X /\ A. x e. A E. v e. U ( v " { x } ) C_ A ) ) )
8		elex	|- ( A e. ~P X -> A e. _V )
9	8	a1i	|- ( U e. ( UnifOn ` X ) -> ( A e. ~P X -> A e. _V ) )
10		elfvex	|- ( U e. ( UnifOn ` X ) -> X e. _V )
11	10	adantr	|- ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> X e. _V )
12		simpr	|- ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> A C_ X )
13	11 12	ssexd	|- ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> A e. _V )
14	13	ex	|- ( U e. ( UnifOn ` X ) -> ( A C_ X -> A e. _V ) )
15		elpwg	|- ( A e. _V -> ( A e. ~P X <-> A C_ X ) )
16	15	a1i	|- ( U e. ( UnifOn ` X ) -> ( A e. _V -> ( A e. ~P X <-> A C_ X ) ) )
17	9 14 16	pm5.21ndd	|- ( U e. ( UnifOn ` X ) -> ( A e. ~P X <-> A C_ X ) )
18	17	anbi1d	|- ( U e. ( UnifOn ` X ) -> ( ( A e. ~P X /\ A. x e. A E. v e. U ( v " { x } ) C_ A ) <-> ( A C_ X /\ A. x e. A E. v e. U ( v " { x } ) C_ A ) ) )
19	7 18	bitrd	|- ( U e. ( UnifOn ` X ) -> ( A e. ( unifTop ` U ) <-> ( A C_ X /\ A. x e. A E. v e. U ( v " { x } ) C_ A ) ) )