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

Theorem reldmmpo 7567
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 7539 . 2 Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 rngop.1 . . . . 5 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
3 df-mpo 7436 . . . . 5 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
42, 3eqtri 2763 . . . 4 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
54dmeqi 5918 . . 3 dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
65releqi 5790 . 2 (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)})
71, 6mpbir 231 1 Rel dom 𝐹
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1537  wcel 2106  dom cdm 5689  Rel wrel 5694  {coprab 7432  cmpo 7433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-dm 5699  df-oprab 7435  df-mpo 7436
This theorem is referenced by:  reldmmap  8874  reldmrelexp  15057  reldmsets  17199  reldmress  17276  reldmprds  17495  gsum0  18710  reldmghm  19245  oppglsm  19675  reldmdprd  20032  reldmlmhm  21042  zrhval  21536  reldmdsmm  21771  frlmrcl  21795  reldmpsr  21952  reldmmpl  22026  reldmopsr  22081  reldmevls  22126  reldmmhp  22159  vr1val  22209  reldmevls1  22337  evl1fval  22348  matbas0pc  22429  mdetfval  22608  madufval  22659  qtopres  23722  fgabs  23903  reldmtng  24667  reldmnghm  24749  reldmnmhm  24750  dvbsss  25952  reldmmdeg  26111  nbgrprc0  29366  wwlksn  29867  of0r  32695  reldmrloc  33244  erlval  33245  reldmresv  33332  bj-restsnid  37070  mzpmfp  42735  brovmptimex  44017  clnbgrprc0  47745  grimdmrel  47804  grlimdmrel  47883  1aryenef  48495  2aryenef  48506
  Copyright terms: Public domain W3C validator