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 ⊢ U ∈ UnifOn ⁡ X → toUnifSp ⁡ U = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U

Proof

Step Hyp Ref Expression
1 df-tus ⊢ toUnifSp = u ∈ ⋃ ran ⁡ UnifOn ⟼ Base ndx dom ⁡ ⋃ u UnifSet ⁡ ndx u sSet TopSet ⁡ ndx unifTop ⁡ u
2 simpr ⊢ U ∈ UnifOn ⁡ X ∧ u = U → u = U
3 2 unieqd ⊢ U ∈ UnifOn ⁡ X ∧ u = U → ⋃ u = ⋃ U
4 3 dmeqd ⊢ U ∈ UnifOn ⁡ X ∧ u = U → dom ⁡ ⋃ u = dom ⁡ ⋃ U
5 4 opeq2d ⊢ U ∈ UnifOn ⁡ X ∧ u = U → Base ndx dom ⁡ ⋃ u = Base ndx dom ⁡ ⋃ U
6 2 opeq2d ⊢ U ∈ UnifOn ⁡ X ∧ u = U → UnifSet ⁡ ndx u = UnifSet ⁡ ndx U
7 5 6 preq12d ⊢ U ∈ UnifOn ⁡ X ∧ u = U → Base ndx dom ⁡ ⋃ u UnifSet ⁡ ndx u = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
8 2 fveq2d ⊢ U ∈ UnifOn ⁡ X ∧ u = U → unifTop ⁡ u = unifTop ⁡ U
9 8 opeq2d ⊢ U ∈ UnifOn ⁡ X ∧ u = U → TopSet ⁡ ndx unifTop ⁡ u = TopSet ⁡ ndx unifTop ⁡ U
10 7 9 oveq12d ⊢ U ∈ UnifOn ⁡ X ∧ u = U → Base ndx dom ⁡ ⋃ u UnifSet ⁡ ndx u sSet TopSet ⁡ ndx unifTop ⁡ u = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
11 elrnust ⊢ U ∈ UnifOn ⁡ X → U ∈ ⋃ ran ⁡ UnifOn
12 ovexd ⊢ U ∈ UnifOn ⁡ X → Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U ∈ V
13 1 10 11 12 fvmptd2 ⊢ U ∈ UnifOn ⁡ X → toUnifSp ⁡ U = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U