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

Metamath Proof Explorer

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 )