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

Theorem reldmmpo 7545
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 7516 . 2 Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 rngop.1 . . . . 5 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
3 df-mpo 7416 . . . . 5 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
42, 3eqtri 2758 . . . 4 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
54dmeqi 5903 . . 3 dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
65releqi 5776 . 2 (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)})
71, 6mpbir 230 1 Rel dom 𝐹
Colors of variables: wff setvar class
Syntax hints:  wa 394   = wceq 1539  wcel 2104  dom cdm 5675  Rel wrel 5680  {coprab 7412  cmpo 7413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-dm 5685  df-oprab 7415  df-mpo 7416
This theorem is referenced by:  reldmmap  8831  reldmrelexp  14972  reldmsets  17102  reldmress  17179  reldmprds  17398  gsum0  18609  reldmghm  19129  oppglsm  19551  reldmdprd  19908  reldmlmhm  20780  zrhval  21276  reldmdsmm  21507  frlmrcl  21531  reldmpsr  21686  reldmmpl  21766  reldmopsr  21819  reldmevls  21866  vr1val  21935  reldmevls1  22056  evl1fval  22067  matbas0pc  22129  mdetfval  22308  madufval  22359  qtopres  23422  fgabs  23603  reldmtng  24367  reldmnghm  24449  reldmnmhm  24450  dvbsss  25651  reldmmdeg  25807  nbgrprc0  28858  wwlksn  29358  reldmresv  32710  bj-restsnid  36271  mzpmfp  41787  brovmptimex  43080  1aryenef  47418  2aryenef  47429
  Copyright terms: Public domain W3C validator