Theorem reldmmpo 7553

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2146  dom cdm 5663  Rel wrel 5668  {coprab 7420   ∈ cmpo 7421

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670  df-dm 5673  df-oprab 7423  df-mpo 7424

This theorem is used by:  reldmmap  8838  reldmrelexp  15084  reldmsets  17249  reldmress  17316  reldmprds  17525  gsum0  18776  reldmghm  19331  oppglsm  19758  reldmdprd  20115  reldmlmhm  21198  zrhval  21709  reldmdsmm  21935  frlmrcl  21959  reldmpsr  22116  reldmmpl  22189  reldmopsr  22248  reldmevls  22287  reldmmhp  22352  vr1val  22404  reldmevls1  22529  evl1fval  22540  matbas0pc  22618  mdetfval  22795  madufval  22846  qtopres  23908  fgabs  24089  reldmtng  24848  reldmnghm  24922  reldmnmhm  24923  dvbsss  26114  reldmmdeg  26267  nbgrprc0  29744  wwlksn  30255  of0r  33097  reldmrloc  33643  erlval  33644  reldmresv  33714  bj-restsnid  37788  mzpmfp  43538  brovmptimex  44813  clnbgrprc0  48645  grimdmrel  48705  grlimdmrel  48805  1aryenef  49484  2aryenef  49495  resccat  49911  reldmfunc  49912  reldmoppf  49962  reldmup  50012  reldmup2  50019  reldmxpcALT  50084  fucofvalne  50162  reldmprcof  50212  reldmprcof2  50219  prcof1  50225  reldmlan  50448  reldmran  50449  reldmlan2  50454  reldmran2  50455  reldmlmd  50484  reldmcmd  50485