This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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