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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | utopval | |
|
2 | 1 | eleq2d | |
3 | sseq2 | |
|
4 | 3 | rexbidv | |
5 | 4 | raleqbi1dv | |
6 | 5 | elrab | |
7 | 2 6 | bitrdi | |
8 | elex | |
|
9 | 8 | a1i | |
10 | elfvex | |
|
11 | 10 | adantr | |
12 | simpr | |
|
13 | 11 12 | ssexd | |
14 | 13 | ex | |
15 | elpwg | |
|
16 | 15 | a1i | |
17 | 9 14 16 | pm5.21ndd | |
18 | 17 | anbi1d | |
19 | 7 18 | bitrd | |