Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 ussval.1 𝐵 = ( Base ‘ 𝑊 )
2 ussval.2 𝑈 = ( UnifSet ‘ 𝑊 )
3 oveq2 ( ( 𝐵 × 𝐵 ) = 𝑈 → ( 𝑈t ( 𝐵 × 𝐵 ) ) = ( 𝑈t 𝑈 ) )
4 id ( ( 𝐵 × 𝐵 ) = 𝑈 → ( 𝐵 × 𝐵 ) = 𝑈 )
5 1 fvexi 𝐵 ∈ V
6 5 5 xpex ( 𝐵 × 𝐵 ) ∈ V
7 4 6 eqeltrrdi ( ( 𝐵 × 𝐵 ) = 𝑈 𝑈 ∈ V )
8 uniexb ( 𝑈 ∈ V ↔ 𝑈 ∈ V )
9 7 8 sylibr ( ( 𝐵 × 𝐵 ) = 𝑈𝑈 ∈ V )
10 eqid 𝑈 = 𝑈
11 10 restid ( 𝑈 ∈ V → ( 𝑈t 𝑈 ) = 𝑈 )
12 9 11 syl ( ( 𝐵 × 𝐵 ) = 𝑈 → ( 𝑈t 𝑈 ) = 𝑈 )
13 3 12 eqtr2d ( ( 𝐵 × 𝐵 ) = 𝑈𝑈 = ( 𝑈t ( 𝐵 × 𝐵 ) ) )
14 1 2 ussval ( 𝑈t ( 𝐵 × 𝐵 ) ) = ( UnifSt ‘ 𝑊 )
15 13 14 eqtrdi ( ( 𝐵 × 𝐵 ) = 𝑈𝑈 = ( UnifSt ‘ 𝑊 ) )