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={\mathrm{Base}}_W$$
	ussval.2	$$⊢U=\mathrm{UnifSet}\left(W\right)$$
Assertion	ussval	$$⊢U{\upharpoonright }_{𝑡}\left(B\times B\right)=\mathrm{UnifSt}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		ussval.1	$$⊢B={\mathrm{Base}}_W$$
2		ussval.2	$$⊢U=\mathrm{UnifSet}\left(W\right)$$
3	1 1	xpeq12i	$$⊢B\times B={\mathrm{Base}}_W\times {\mathrm{Base}}_W$$
4	2 3	oveq12i	$$⊢U{\upharpoonright }_{𝑡}\left(B\times B\right)=\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)$$
5		fveq2	$$⊢w=W\to \mathrm{UnifSet}\left(w\right)=\mathrm{UnifSet}\left(W\right)$$
6		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
7	6	sqxpeqd	$$⊢w=W\to {\mathrm{Base}}_w\times {\mathrm{Base}}_w={\mathrm{Base}}_W\times {\mathrm{Base}}_W$$
8	5 7	oveq12d	$$⊢w=W\to \mathrm{UnifSet}\left(w\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_w\times {\mathrm{Base}}_w\right)=\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)$$
9		df-uss	$$⊢\mathrm{UnifSt}=\left(w\in \mathrm{V}⟼\mathrm{UnifSet}\left(w\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_w\times {\mathrm{Base}}_w\right)\right)$$
10		ovex	$$⊢\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)\in \mathrm{V}$$
11	8 9 10	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{UnifSt}\left(W\right)=\mathrm{UnifSet}\left(W\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_W\times {\mathrm{Base}}_W\right)$$
12	4 11	eqtr4id	$$⊢W\in \mathrm{V}\to U{\upharpoonright }_{𝑡}\left(B\times B\right)=\mathrm{UnifSt}\left(W\right)$$
13		0rest	$$⊢\varnothing {\upharpoonright }_{𝑡}\left(B\times B\right)=\varnothing$$
14		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{UnifSet}\left(W\right)=\varnothing$$
15	2 14	syl5eq	$$⊢\neg W\in \mathrm{V}\to U=\varnothing$$
16	15	oveq1d	$$⊢\neg W\in \mathrm{V}\to U{\upharpoonright }_{𝑡}\left(B\times B\right)=\varnothing {\upharpoonright }_{𝑡}\left(B\times B\right)$$
17		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{UnifSt}\left(W\right)=\varnothing$$
18	13 16 17	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to U{\upharpoonright }_{𝑡}\left(B\times B\right)=\mathrm{UnifSt}\left(W\right)$$
19	12 18	pm2.61i	$$⊢U{\upharpoonright }_{𝑡}\left(B\times B\right)=\mathrm{UnifSt}\left(W\right)$$