Theorem reldmmpo 7530

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 7503	. 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		rngop.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
3		df-mpo 7401	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
4	2, 3	eqtri 2785	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
5	4	dmeqi 5880	. . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
6	5	releqi 5750	. 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)})
7	1, 6	mpbir 233	1 ⊢ Rel dom 𝐹

Syntax hints:   ∧ wa 399   = wceq 1560   ∈ wcel 2142  dom cdm 5647  Rel wrel 5652  {coprab 7397   ∈ cmpo 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-rel 5654  df-dm 5657  df-oprab 7400  df-mpo 7401

This theorem is referenced by:  reldmmap  8816  reldmrelexp  15034  reldmsets  17201  reldmress  17268  reldmprds  17477  gsum0  18718  reldmghm  19255  oppglsm  19682  reldmdprd  20039  reldmlmhm  21092  zrhval  21559  reldmdsmm  21785  frlmrcl  21809  reldmpsr  21966  reldmmpl  22039  reldmopsr  22098  reldmevls  22137  reldmmhp  22202  vr1val  22254  reldmevls1  22380  evl1fval  22391  matbas0pc  22469  mdetfval  22646  madufval  22697  qtopres  23758  fgabs  23939  reldmtng  24698  reldmnghm  24772  reldmnmhm  24773  dvbsss  25964  reldmmdeg  26117  nbgrprc0  29535  wwlksn  30037  of0r  32881  reldmrloc  33438  erlval  33439  reldmresv  33514  bj-restsnid  37577  mzpmfp  43328  brovmptimex  44603  clnbgrprc0  48442  grimdmrel  48502  grlimdmrel  48602  1aryenef  49267  2aryenef  49278  resccat  49695  reldmfunc  49696  reldmoppf  49746  reldmup  49796  reldmup2  49803  reldmxpcALT  49868  fucofvalne  49946  reldmprcof  49996  reldmprcof2  50003  prcof1  50009  reldmlan  50232  reldmran  50233  reldmlan2  50238  reldmran2  50239  reldmlmd  50268  reldmcmd  50269