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 ⊢ 𝐾 = ( toUnifSp ‘ 𝑈 )
Assertion tususs ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 = ( UnifSt ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 tuslem.k ⊢ 𝐾 = ( toUnifSp ‘ 𝑈 )
2 1 tusunif ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 = ( UnifSet ‘ 𝐾 ) )
3 ustuni ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ 𝑈 = ( 𝑋 × 𝑋 ) )
4 2 unieqd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ 𝑈 = ∪ ( UnifSet ‘ 𝐾 ) )
5 1 tusbas ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )
6 5 sqxpeqd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
7 3 4 6 3eqtr3rd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) = ∪ ( UnifSet ‘ 𝐾 ) )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 eqid ⊢ ( UnifSet ‘ 𝐾 ) = ( UnifSet ‘ 𝐾 )
10 8 9 ussid ⊢ ( ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) = ∪ ( UnifSet ‘ 𝐾 ) → ( UnifSet ‘ 𝐾 ) = ( UnifSt ‘ 𝐾 ) )
11 7 10 syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( UnifSet ‘ 𝐾 ) = ( UnifSt ‘ 𝐾 ) )
12 2 11 eqtrd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 = ( UnifSt ‘ 𝐾 ) )