Theorem reldmmpo 7544

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 7517	. 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		rngop.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
3		df-mpo 7415	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
4	2, 3	eqtri 2786	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
5	4	dmeqi 5894	. . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
6	5	releqi 5764	. 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)})
7	1, 6	mpbir 234	1 ⊢ Rel dom 𝐹

Syntax hints:   ∧ wa 400   = wceq 1570   ∈ wcel 2143  dom cdm 5661  Rel wrel 5666  {coprab 7411   ∈ cmpo 7412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-dm 5671  df-oprab 7414  df-mpo 7415

This theorem is referenced by:  reldmmap  8828  reldmrelexp  15054  reldmsets  17220  reldmress  17287  reldmprds  17496  gsum0  18737  reldmghm  19280  oppglsm  19707  reldmdprd  20064  reldmlmhm  21146  zrhval  21657  reldmdsmm  21883  frlmrcl  21907  reldmpsr  22064  reldmmpl  22137  reldmopsr  22196  reldmevls  22235  reldmmhp  22300  vr1val  22352  reldmevls1  22477  evl1fval  22488  matbas0pc  22566  mdetfval  22743  madufval  22794  qtopres  23855  fgabs  24036  reldmtng  24795  reldmnghm  24869  reldmnmhm  24870  dvbsss  26061  reldmmdeg  26214  nbgrprc0  29684  wwlksn  30186  of0r  33024  reldmrloc  33577  erlval  33578  reldmresv  33648  bj-restsnid  37749  mzpmfp  43498  brovmptimex  44773  clnbgrprc0  48605  grimdmrel  48665  grlimdmrel  48765  1aryenef  49445  2aryenef  49456  resccat  49872  reldmfunc  49873  reldmoppf  49923  reldmup  49973  reldmup2  49980  reldmxpcALT  50045  fucofvalne  50123  reldmprcof  50173  reldmprcof2  50180  prcof1  50186  reldmlan  50409  reldmran  50410  reldmlan2  50415  reldmran2  50416  reldmlmd  50445  reldmcmd  50446