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 elrnust ( 𝑈 ∈ ( 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 ‘ 𝑈 ) ⟩ ) )