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

Theorem reldmmpo 7546
Description: The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
Hypothesis
Ref Expression
rngop.1 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
Assertion
Ref Expression
reldmmpo Rel dom 𝐹
Distinct variable groups:   𝑦,𝐴   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem reldmmpo
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 reldmoprab 7517 . 2 Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 rngop.1 . . . . 5 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
3 df-mpo 7417 . . . . 5 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
42, 3eqtri 2759 . . . 4 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
54dmeqi 5904 . . 3 dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
65releqi 5777 . 2 (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)})
71, 6mpbir 230 1 Rel dom 𝐹
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1540  wcel 2105  dom cdm 5676  Rel wrel 5681  {coprab 7413  cmpo 7414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-dm 5686  df-oprab 7416  df-mpo 7417
This theorem is referenced by:  reldmmap  8832  reldmrelexp  14973  reldmsets  17103  reldmress  17180  reldmprds  17399  gsum0  18610  reldmghm  19130  oppglsm  19552  reldmdprd  19909  reldmlmhm  20781  zrhval  21277  reldmdsmm  21508  frlmrcl  21532  reldmpsr  21687  reldmmpl  21767  reldmopsr  21820  reldmevls  21867  vr1val  21936  reldmevls1  22057  evl1fval  22068  matbas0pc  22130  mdetfval  22309  madufval  22360  qtopres  23423  fgabs  23604  reldmtng  24368  reldmnghm  24450  reldmnmhm  24451  dvbsss  25652  reldmmdeg  25808  nbgrprc0  28859  wwlksn  29359  reldmresv  32711  bj-restsnid  36272  mzpmfp  41788  brovmptimex  43081  1aryenef  47419  2aryenef  47430
  Copyright terms: Public domain W3C validator