Theorem reldmmpo 7490

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.

Step	Hyp	Ref	Expression
1		reldmoprab 7463	. 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		rngop.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
3		df-mpo 7361	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
4	2, 3	eqtri 2762	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
5	4	dmeqi 5846	. . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
6	5	releqi 5721	. 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)})
7	1, 6	mpbir 232	1 ⊢ Rel dom 𝐹

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119  dom cdm 5618  Rel wrel 5623  {coprab 7357   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-dm 5628  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  reldmmap  8772  reldmrelexp  14974  reldmsets  17126  reldmress  17193  reldmprds  17402  gsum0  18643  reldmghm  19180  oppglsm  19608  reldmdprd  19965  reldmlmhm  21015  zrhval  21482  reldmdsmm  21708  frlmrcl  21732  reldmpsr  21889  reldmmpl  21962  reldmopsr  22021  reldmevls  22060  reldmmhp  22125  vr1val  22177  reldmevls1  22303  evl1fval  22314  matbas0pc  22392  mdetfval  22569  madufval  22620  qtopres  23681  fgabs  23862  reldmtng  24621  reldmnghm  24695  reldmnmhm  24696  dvbsss  25887  reldmmdeg  26040  nbgrprc0  29421  wwlksn  29923  of0r  32771  reldmrloc  33338  erlval  33339  reldmresv  33411  bj-restsnid  37445  mzpmfp  43196  brovmptimex  44471  clnbgrprc0  48311  grimdmrel  48371  grlimdmrel  48471  1aryenef  49136  2aryenef  49147  resccat  49564  reldmfunc  49565  reldmoppf  49615  reldmup  49665  reldmup2  49672  reldmxpcALT  49737  fucofvalne  49815  reldmprcof  49865  reldmprcof2  49872  prcof1  49878  reldmlan  50101  reldmran  50102  reldmlan2  50107  reldmran2  50108  reldmlmd  50137  reldmcmd  50138