Theorem tususp

Description: A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

	Ref	Expression
Hypothesis	tuslem.k	⊢ 𝐾 = ( toUnifSp ‘ 𝑈 )
Assertion	tususp	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐾 ∈ UnifSp )

Proof

Step	Hyp	Ref	Expression
1		tuslem.k	⊢ 𝐾 = ( toUnifSp ‘ 𝑈 )
2		id	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
3	1	tususs	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 = ( UnifSt ‘ 𝐾 ) )
4	1	tusbas	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )
5	4	fveq2d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( UnifOn ‘ 𝑋 ) = ( UnifOn ‘ ( Base ‘ 𝐾 ) ) )
6	2 3 5	3eltr3d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( UnifSt ‘ 𝐾 ) ∈ ( UnifOn ‘ ( Base ‘ 𝐾 ) ) )
7	1	tusunif	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 = ( UnifSet ‘ 𝐾 ) )
8	7	fveq2d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = ( unifTop ‘ ( UnifSet ‘ 𝐾 ) ) )
9	1	tuslem	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 = ( Base ‘ 𝐾 ) ∧ 𝑈 = ( UnifSet ‘ 𝐾 ) ∧ ( unifTop ‘ 𝑈 ) = ( TopOpen ‘ 𝐾 ) ) )
10	9	simp3d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = ( TopOpen ‘ 𝐾 ) )
11	7 3	eqtr3d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( UnifSet ‘ 𝐾 ) = ( UnifSt ‘ 𝐾 ) )
12	11	fveq2d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ ( UnifSet ‘ 𝐾 ) ) = ( unifTop ‘ ( UnifSt ‘ 𝐾 ) ) )
13	8 10 12	3eqtr3d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( TopOpen ‘ 𝐾 ) = ( unifTop ‘ ( UnifSt ‘ 𝐾 ) ) )
14		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15		eqid	⊢ ( UnifSt ‘ 𝐾 ) = ( UnifSt ‘ 𝐾 )
16		eqid	⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
17	14 15 16	isusp	⊢ ( 𝐾 ∈ UnifSp ↔ ( ( UnifSt ‘ 𝐾 ) ∈ ( UnifOn ‘ ( Base ‘ 𝐾 ) ) ∧ ( TopOpen ‘ 𝐾 ) = ( unifTop ‘ ( UnifSt ‘ 𝐾 ) ) ) )
18	6 13 17	sylanbrc	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐾 ∈ UnifSp )