This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ 𝑊 ∈ 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 ‘ 𝑊 )