Metamath Proof Explorer


Theorem isusp

Description: The predicate W is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017)

Ref Expression
Hypotheses isusp.1 B=BaseW
isusp.2 U=UnifStW
isusp.3 J=TopOpenW
Assertion isusp WUnifSpUUnifOnBJ=unifTopU

Proof

Step Hyp Ref Expression
1 isusp.1 B=BaseW
2 isusp.2 U=UnifStW
3 isusp.3 J=TopOpenW
4 elex WUnifSpWV
5 0nep0
6 fvprc ¬WVBaseW=
7 1 6 eqtrid ¬WVB=
8 7 fveq2d ¬WVUnifOnB=UnifOn
9 ust0 UnifOn=
10 8 9 eqtrdi ¬WVUnifOnB=
11 10 eleq2d ¬WVUUnifOnBU
12 2 fvexi UV
13 12 elsn UU=
14 11 13 bitrdi ¬WVUUnifOnBU=
15 fvprc ¬WVUnifStW=
16 2 15 eqtrid ¬WVU=
17 16 eqeq1d ¬WVU==
18 14 17 bitrd ¬WVUUnifOnB=
19 18 necon3bbid ¬WV¬UUnifOnB
20 5 19 mpbiri ¬WV¬UUnifOnB
21 20 con4i UUnifOnBWV
22 21 adantr UUnifOnBJ=unifTopUWV
23 fveq2 w=WUnifStw=UnifStW
24 23 2 eqtr4di w=WUnifStw=U
25 fveq2 w=WBasew=BaseW
26 25 1 eqtr4di w=WBasew=B
27 26 fveq2d w=WUnifOnBasew=UnifOnB
28 24 27 eleq12d w=WUnifStwUnifOnBasewUUnifOnB
29 fveq2 w=WTopOpenw=TopOpenW
30 29 3 eqtr4di w=WTopOpenw=J
31 24 fveq2d w=WunifTopUnifStw=unifTopU
32 30 31 eqeq12d w=WTopOpenw=unifTopUnifStwJ=unifTopU
33 28 32 anbi12d w=WUnifStwUnifOnBasewTopOpenw=unifTopUnifStwUUnifOnBJ=unifTopU
34 df-usp UnifSp=w|UnifStwUnifOnBasewTopOpenw=unifTopUnifStw
35 33 34 elab2g WVWUnifSpUUnifOnBJ=unifTopU
36 4 22 35 pm5.21nii WUnifSpUUnifOnBJ=unifTopU