Theorem ussval

Description: The uniform structure on uniform space W . This proof uses a trick with fvprc to avoid requiring W to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		ussval.1	|- B = ( Base ` W )
2		ussval.2	|- U = ( UnifSet ` W )
3	1 1	xpeq12i	|- ( B X. B ) = ( ( Base ` W ) X. ( Base ` W ) )
4	2 3	oveq12i	|- ( U |`t ( B X. B ) ) = ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) )
5		fveq2	|- ( w = W -> ( UnifSet ` w ) = ( UnifSet ` W ) )
6		fveq2	|- ( w = W -> ( Base ` w ) = ( Base ` W ) )
7	6	sqxpeqd	|- ( w = W -> ( ( Base ` w ) X. ( Base ` w ) ) = ( ( Base ` W ) X. ( Base ` W ) ) )
8	5 7	oveq12d	|- ( w = W -> ( ( UnifSet ` w ) |`t ( ( Base ` w ) X. ( Base ` w ) ) ) = ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) )
9		df-uss	|- UnifSt = ( w e. _V |-> ( ( UnifSet ` w ) |`t ( ( Base ` w ) X. ( Base ` w ) ) ) )
10		ovex	|- ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) e. _V
11	8 9 10	fvmpt	|- ( W e. _V -> ( UnifSt ` W ) = ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) )
12	4 11	eqtr4id	|- ( W e. _V -> ( U |`t ( B X. B ) ) = ( UnifSt ` W ) )
13		0rest	|- ( (/) |`t ( B X. B ) ) = (/)
14		fvprc	|- ( -. W e. _V -> ( UnifSet ` W ) = (/) )
15	2 14	syl5eq	|- ( -. W e. _V -> U = (/) )
16	15	oveq1d	|- ( -. W e. _V -> ( U |`t ( B X. B ) ) = ( (/) |`t ( B X. B ) ) )
17		fvprc	|- ( -. W e. _V -> ( UnifSt ` W ) = (/) )
18	13 16 17	3eqtr4a	|- ( -. W e. _V -> ( U |`t ( B X. B ) ) = ( UnifSt ` W ) )
19	12 18	pm2.61i	|- ( U |`t ( B X. B ) ) = ( UnifSt ` W )