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

Metamath Proof Explorer

Theorem ussid

Description: In case the base of the UnifSt element of the uniform space is the base of its element structure, then UnifSt does not restrict it further. (Contributed by Thierry Arnoux, 4-Dec-2017)

Ref Expression
Hypotheses ussval.1 
|- B = ( Base ` W )
ussval.2 
|- U = ( UnifSet ` W )
Assertion ussid 
|- ( ( B X. B ) = U. U -> U = ( UnifSt ` W ) )

Proof

Step Hyp Ref Expression
1 ussval.1 
 |-  B = ( Base ` W )
2 ussval.2 
 |-  U = ( UnifSet ` W )
3 oveq2 
 |-  ( ( B X. B ) = U. U -> ( U |`t ( B X. B ) ) = ( U |`t U. U ) )
4 id 
 |-  ( ( B X. B ) = U. U -> ( B X. B ) = U. U )
5 1 fvexi 
 |-  B e. _V
6 5 5 xpex 
 |-  ( B X. B ) e. _V
7 4 6 eqeltrrdi 
 |-  ( ( B X. B ) = U. U -> U. U e. _V )
8 uniexb 
 |-  ( U e. _V <-> U. U e. _V )
9 7 8 sylibr 
 |-  ( ( B X. B ) = U. U -> U e. _V )
10 eqid 
 |-  U. U = U. U
11 10 restid 
 |-  ( U e. _V -> ( U |`t U. U ) = U )
12 9 11 syl 
 |-  ( ( B X. B ) = U. U -> ( U |`t U. U ) = U )
13 3 12 eqtr2d 
 |-  ( ( B X. B ) = U. U -> U = ( U |`t ( B X. B ) ) )
14 1 2 ussval 
 |-  ( U |`t ( B X. B ) ) = ( UnifSt ` W )
15 13 14 eqtrdi 
 |-  ( ( B X. B ) = U. U -> U = ( UnifSt ` W ) )