Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tusval Structured version   Visualization version   GIF version

Theorem tusval 22960
 Description: The value of the uniform space mapping function. (Contributed by Thierry Arnoux, 5-Dec-2017.)
Assertion
Ref Expression
tusval (𝑈 ∈ (UnifOn‘𝑋) → (toUnifSp‘𝑈) = ({⟨(Base‘ndx), dom 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))

Proof of Theorem tusval
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 df-tus 22952 . 2 toUnifSp = (𝑢 ran UnifOn ↦ ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))
2 simpr 489 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 = 𝑈) → 𝑢 = 𝑈)
32unieqd 4813 . . . . . 6 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 = 𝑈) → 𝑢 = 𝑈)
43dmeqd 5746 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 = 𝑈) → dom 𝑢 = dom 𝑈)
54opeq2d 4771 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 = 𝑈) → ⟨(Base‘ndx), dom 𝑢⟩ = ⟨(Base‘ndx), dom 𝑈⟩)
62opeq2d 4771 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 = 𝑈) → ⟨(UnifSet‘ndx), 𝑢⟩ = ⟨(UnifSet‘ndx), 𝑈⟩)
75, 6preq12d 4635 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 = 𝑈) → {⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} = {⟨(Base‘ndx), dom 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩})
82fveq2d 6663 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 = 𝑈) → (unifTop‘𝑢) = (unifTop‘𝑈))
98opeq2d 4771 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 = 𝑈) → ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩ = ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)
107, 9oveq12d 7169 . 2 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 = 𝑈) → ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩) = ({⟨(Base‘ndx), dom 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
11 elrnust 22918 . 2 (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ran UnifOn)
12 ovexd 7186 . 2 (𝑈 ∈ (UnifOn‘𝑋) → ({⟨(Base‘ndx), dom 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩) ∈ V)
131, 10, 11, 12fvmptd2 6768 1 (𝑈 ∈ (UnifOn‘𝑋) → (toUnifSp‘𝑈) = ({⟨(Base‘ndx), dom 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  Vcvv 3410  {cpr 4525  ⟨cop 4529  ∪ cuni 4799  dom cdm 5525  ran crn 5526  ‘cfv 6336  (class class class)co 7151  ndxcnx 16531   sSet csts 16532  Basecbs 16534  TopSetcts 16622  UnifSetcunif 16626  UnifOncust 22893  unifTopcutop 22924  toUnifSpctus 22949 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-iota 6295  df-fun 6338  df-fn 6339  df-fv 6344  df-ov 7154  df-ust 22894  df-tus 22952 This theorem is referenced by:  tuslem  22961
 Copyright terms: Public domain W3C validator