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

Metamath Proof Explorer

Theorem tususs

Description: The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017)

Ref Expression
Hypothesis tuslem.k ⊢ K = toUnifSp ⁡ U
Assertion tususs ⊢ U ∈ UnifOn ⁡ X → U = UnifSt ⁡ K

Proof

Step Hyp Ref Expression
1 tuslem.k ⊢ K = toUnifSp ⁡ U
2 1 tusunif ⊢ U ∈ UnifOn ⁡ X → U = UnifSet ⁡ K
3 ustuni ⊢ U ∈ UnifOn ⁡ X → ⋃ U = X × X
4 2 unieqd ⊢ U ∈ UnifOn ⁡ X → ⋃ U = ⋃ UnifSet ⁡ K
5 1 tusbas ⊢ U ∈ UnifOn ⁡ X → X = Base K
6 5 sqxpeqd ⊢ U ∈ UnifOn ⁡ X → X × X = Base K × Base K
7 3 4 6 3eqtr3rd ⊢ U ∈ UnifOn ⁡ X → Base K × Base K = ⋃ UnifSet ⁡ K
8 eqid ⊢ Base K = Base K
9 eqid ⊢ UnifSet ⁡ K = UnifSet ⁡ K
10 8 9 ussid ⊢ Base K × Base K = ⋃ UnifSet ⁡ K → UnifSet ⁡ K = UnifSt ⁡ K
11 7 10 syl ⊢ U ∈ UnifOn ⁡ X → UnifSet ⁡ K = UnifSt ⁡ K
12 2 11 eqtrd ⊢ U ∈ UnifOn ⁡ X → U = UnifSt ⁡ K