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

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 ⊢ B = Base W
ussval.2 ⊢ U = UnifSet ⁡ W
Assertion ussid ⊢ B × B = ⋃ U → U = UnifSt ⁡ W

Proof

Step Hyp Ref Expression
1 ussval.1 ⊢ B = Base W
2 ussval.2 ⊢ U = UnifSet ⁡ W
3 oveq2 ⊢ B × B = ⋃ U → U ↾ 𝑡 B × B = U ↾ 𝑡 ⋃ U
4 id ⊢ B × B = ⋃ U → B × B = ⋃ U
5 1 fvexi ⊢ B ∈ V
6 5 5 xpex ⊢ B × B ∈ V
7 4 6 eqeltrrdi ⊢ B × B = ⋃ U → ⋃ U ∈ V
8 uniexb ⊢ U ∈ V ↔ ⋃ U ∈ V
9 7 8 sylibr ⊢ B × B = ⋃ U → U ∈ V
10 eqid ⊢ ⋃ U = ⋃ U
11 10 restid ⊢ U ∈ V → U ↾ 𝑡 ⋃ U = U
12 9 11 syl ⊢ B × B = ⋃ U → U ↾ 𝑡 ⋃ U = U
13 3 12 eqtr2d ⊢ B × B = ⋃ U → U = U ↾ 𝑡 B × B
14 1 2 ussval ⊢ U ↾ 𝑡 B × B = UnifSt ⁡ W
15 13 14 eqtrdi ⊢ B × B = ⋃ U → U = UnifSt ⁡ W