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 = ( Base ` W )
isusp.2 
|- U = ( UnifSt ` W )
isusp.3 
|- J = ( TopOpen ` W )
Assertion isusp 
|- ( W e. UnifSp <-> ( U e. ( UnifOn ` B ) /\ J = ( unifTop ` U ) ) )

Proof

Step Hyp Ref Expression
1 isusp.1 
 |-  B = ( Base ` W )
2 isusp.2 
 |-  U = ( UnifSt ` W )
3 isusp.3 
 |-  J = ( TopOpen ` W )
4 elex 
 |-  ( W e. UnifSp -> W e. _V )
5 0nep0 
 |-  (/) =/= { (/) }
6 fvprc 
 |-  ( -. W e. _V -> ( Base ` W ) = (/) )
7 1 6 syl5eq 
 |-  ( -. W e. _V -> B = (/) )
8 7 fveq2d 
 |-  ( -. W e. _V -> ( UnifOn ` B ) = ( UnifOn ` (/) ) )
9 ust0 
 |-  ( UnifOn ` (/) ) = { { (/) } }
10 8 9 eqtrdi 
 |-  ( -. W e. _V -> ( UnifOn ` B ) = { { (/) } } )
11 10 eleq2d 
 |-  ( -. W e. _V -> ( U e. ( UnifOn ` B ) <-> U e. { { (/) } } ) )
12 2 fvexi 
 |-  U e. _V
13 12 elsn 
 |-  ( U e. { { (/) } } <-> U = { (/) } )
14 11 13 bitrdi 
 |-  ( -. W e. _V -> ( U e. ( UnifOn ` B ) <-> U = { (/) } ) )
15 fvprc 
 |-  ( -. W e. _V -> ( UnifSt ` W ) = (/) )
16 2 15 syl5eq 
 |-  ( -. W e. _V -> U = (/) )
17 16 eqeq1d 
 |-  ( -. W e. _V -> ( U = { (/) } <-> (/) = { (/) } ) )
18 14 17 bitrd 
 |-  ( -. W e. _V -> ( U e. ( UnifOn ` B ) <-> (/) = { (/) } ) )
19 18 necon3bbid 
 |-  ( -. W e. _V -> ( -. U e. ( UnifOn ` B ) <-> (/) =/= { (/) } ) )
20 5 19 mpbiri 
 |-  ( -. W e. _V -> -. U e. ( UnifOn ` B ) )
21 20 con4i 
 |-  ( U e. ( UnifOn ` B ) -> W e. _V )
22 21 adantr 
 |-  ( ( U e. ( UnifOn ` B ) /\ J = ( unifTop ` U ) ) -> W e. _V )
23 fveq2 
 |-  ( w = W -> ( UnifSt ` w ) = ( UnifSt ` W ) )
24 23 2 eqtr4di 
 |-  ( w = W -> ( UnifSt ` w ) = U )
25 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
26 25 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = B )
27 26 fveq2d 
 |-  ( w = W -> ( UnifOn ` ( Base ` w ) ) = ( UnifOn ` B ) )
28 24 27 eleq12d 
 |-  ( w = W -> ( ( UnifSt ` w ) e. ( UnifOn ` ( Base ` w ) ) <-> U e. ( UnifOn ` B ) ) )
29 fveq2 
 |-  ( w = W -> ( TopOpen ` w ) = ( TopOpen ` W ) )
30 29 3 eqtr4di 
 |-  ( w = W -> ( TopOpen ` w ) = J )
31 24 fveq2d 
 |-  ( w = W -> ( unifTop ` ( UnifSt ` w ) ) = ( unifTop ` U ) )
32 30 31 eqeq12d 
 |-  ( w = W -> ( ( TopOpen ` w ) = ( unifTop ` ( UnifSt ` w ) ) <-> J = ( unifTop ` U ) ) )
33 28 32 anbi12d 
 |-  ( w = W -> ( ( ( UnifSt ` w ) e. ( UnifOn ` ( Base ` w ) ) /\ ( TopOpen ` w ) = ( unifTop ` ( UnifSt ` w ) ) ) <-> ( U e. ( UnifOn ` B ) /\ J = ( unifTop ` U ) ) ) )
34 df-usp 
 |-  UnifSp = { w | ( ( UnifSt ` w ) e. ( UnifOn ` ( Base ` w ) ) /\ ( TopOpen ` w ) = ( unifTop ` ( UnifSt ` w ) ) ) }
35 33 34 elab2g 
 |-  ( W e. _V -> ( W e. UnifSp <-> ( U e. ( UnifOn ` B ) /\ J = ( unifTop ` U ) ) ) )
36 4 22 35 pm5.21nii 
 |-  ( W e. UnifSp <-> ( U e. ( UnifOn ` B ) /\ J = ( unifTop ` U ) ) )