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 ‘ 𝐾 ) )