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={\mathrm{Base}}_W$$
	ussval.2	$$⊢U=\mathrm{UnifSet}\left(W\right)$$
Assertion	ussid	$$⊢B\times B=\bigcup U\to U=\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		oveq2	$$⊢B\times B=\bigcup U\to U{\upharpoonright }_{𝑡}\left(B\times B\right)=U{\upharpoonright }_{𝑡}\bigcup U$$
4		id	$$⊢B\times B=\bigcup U\to B\times B=\bigcup U$$
5	1	fvexi	$$⊢B\in \mathrm{V}$$
6	5 5	xpex	$$⊢B\times B\in \mathrm{V}$$
7	4 6	eqeltrrdi	$$⊢B\times B=\bigcup U\to \bigcup U\in \mathrm{V}$$
8		uniexb	$$⊢U\in \mathrm{V}\leftrightarrow \bigcup U\in \mathrm{V}$$
9	7 8	sylibr	$$⊢B\times B=\bigcup U\to U\in \mathrm{V}$$
10		eqid	$$⊢\bigcup U=\bigcup U$$
11	10	restid	$$⊢U\in \mathrm{V}\to U{\upharpoonright }_{𝑡}\bigcup U=U$$
12	9 11	syl	$$⊢B\times B=\bigcup U\to U{\upharpoonright }_{𝑡}\bigcup U=U$$
13	3 12	eqtr2d	$$⊢B\times B=\bigcup U\to U=U{\upharpoonright }_{𝑡}\left(B\times B\right)$$
14	1 2	ussval	$$⊢U{\upharpoonright }_{𝑡}\left(B\times B\right)=\mathrm{UnifSt}\left(W\right)$$
15	13 14	eqtrdi	$$⊢B\times B=\bigcup U\to U=\mathrm{UnifSt}\left(W\right)$$