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

Metamath Proof Explorer

Theorem tusval

Description: The value of the uniform space mapping function. (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Assertion tusval ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( toUnifSp ‘ 𝑈 ) = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 df-tus ⊢ toUnifSp = ( 𝑢 ∈ ∪ ran UnifOn ↦ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ ) )
2 simpr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 𝑢 = 𝑈 )
3 2 unieqd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ∪ 𝑢 = ∪ 𝑈 )
4 3 dmeqd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → dom ∪ 𝑢 = dom ∪ 𝑈 )
5 4 opeq2d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ = ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ )
6 2 opeq2d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ = ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ )
7 5 6 preq12d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } = { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } )
8 2 fveq2d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( unifTop ‘ 𝑢 ) = ( unifTop ‘ 𝑈 ) )
9 8 opeq2d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ = ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ )
10 7 9 oveq12d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑢 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑢 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) ⟩ ) = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
11 elfvunirn ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn )
12 ovexd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ∈ V )
13 1 10 11 12 fvmptd2 ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( toUnifSp ‘ 𝑈 ) = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )