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 UUnifOnXAunifTopUAXxAvUvxA

Proof

Step Hyp Ref Expression
1 utopval UUnifOnXunifTopU=a𝒫X|xavUvxa
2 1 eleq2d UUnifOnXAunifTopUAa𝒫X|xavUvxa
3 sseq2 a=AvxavxA
4 3 rexbidv a=AvUvxavUvxA
5 4 raleqbi1dv a=AxavUvxaxAvUvxA
6 5 elrab Aa𝒫X|xavUvxaA𝒫XxAvUvxA
7 2 6 bitrdi UUnifOnXAunifTopUA𝒫XxAvUvxA
8 elex A𝒫XAV
9 8 a1i UUnifOnXA𝒫XAV
10 elfvex UUnifOnXXV
11 10 adantr UUnifOnXAXXV
12 simpr UUnifOnXAXAX
13 11 12 ssexd UUnifOnXAXAV
14 13 ex UUnifOnXAXAV
15 elpwg AVA𝒫XAX
16 15 a1i UUnifOnXAVA𝒫XAX
17 9 14 16 pm5.21ndd UUnifOnXA𝒫XAX
18 17 anbi1d UUnifOnXA𝒫XxAvUvxAAXxAvUvxA
19 7 18 bitrd UUnifOnXAunifTopUAXxAvUvxA