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 ) )