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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	ussval.2	⊢ 𝑈 = ( UnifSet ‘ 𝑊 )
Assertion	ussval	⊢ ( 𝑈 ↾t ( 𝐵 × 𝐵 ) ) = ( UnifSt ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		ussval.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		ussval.2	⊢ 𝑈 = ( UnifSet ‘ 𝑊 )
3	1 1	xpeq12i	⊢ ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) )
4	2 3	oveq12i	⊢ ( 𝑈 ↾t ( 𝐵 × 𝐵 ) ) = ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) )
5		fveq2	⊢ ( 𝑤 = 𝑊 → ( UnifSet ‘ 𝑤 ) = ( UnifSet ‘ 𝑊 ) )
6		fveq2	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
7	6	sqxpeqd	⊢ ( 𝑤 = 𝑊 → ( ( Base ‘ 𝑤 ) × ( Base ‘ 𝑤 ) ) = ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) )
8	5 7	oveq12d	⊢ ( 𝑤 = 𝑊 → ( ( UnifSet ‘ 𝑤 ) ↾t ( ( Base ‘ 𝑤 ) × ( Base ‘ 𝑤 ) ) ) = ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) )
9		df-uss	⊢ UnifSt = ( 𝑤 ∈ V ↦ ( ( UnifSet ‘ 𝑤 ) ↾t ( ( Base ‘ 𝑤 ) × ( Base ‘ 𝑤 ) ) ) )
10		ovex	⊢ ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ V
11	8 9 10	fvmpt	⊢ ( 𝑊 ∈ V → ( UnifSt ‘ 𝑊 ) = ( ( UnifSet ‘ 𝑊 ) ↾t ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) )
12	4 11	eqtr4id	⊢ ( 𝑊 ∈ V → ( 𝑈 ↾t ( 𝐵 × 𝐵 ) ) = ( UnifSt ‘ 𝑊 ) )
13		0rest	⊢ ( ∅ ↾t ( 𝐵 × 𝐵 ) ) = ∅
14		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( UnifSet ‘ 𝑊 ) = ∅ )
15	2 14	syl5eq	⊢ ( ¬ 𝑊 ∈ V → 𝑈 = ∅ )
16	15	oveq1d	⊢ ( ¬ 𝑊 ∈ V → ( 𝑈 ↾t ( 𝐵 × 𝐵 ) ) = ( ∅ ↾t ( 𝐵 × 𝐵 ) ) )
17		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( UnifSt ‘ 𝑊 ) = ∅ )
18	13 16 17	3eqtr4a	⊢ ( ¬ 𝑊 ∈ V → ( 𝑈 ↾t ( 𝐵 × 𝐵 ) ) = ( UnifSt ‘ 𝑊 ) )
19	12 18	pm2.61i	⊢ ( 𝑈 ↾t ( 𝐵 × 𝐵 ) ) = ( UnifSt ‘ 𝑊 )