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