Theorem reldmmpo 7584

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
reldmmpo.1	⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

Assertion

Ref	Expression
reldmmpo	⊢ Rel dom 𝐹

Proof of Theorem reldmmpo

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		reldmoprab 7558	. 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		reldmmpo.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
3		df-mpo 7456	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
4	2, 3	eqtri 2786	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
5	4	dmeqi 5898	. . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
6	5	releqi 5762	. 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)})
7	1, 6	mpbir 234	1 ⊢ Rel dom 𝐹

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147  dom cdm 5658  Rel wrel 5663  {coprab 7452   ∈ cmpo 7453

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-dm 5668  df-oprab 7455  df-mpo 7456

This theorem is used by:  reldmmap  8893  reldmrelexp  15217  reldmsets  17387  reldmress  17454  reldmprds  17669  gsum0  18923  reldmghm  19479  oppglsm  19907  reldmdprd  20264  reldmlmhm  21351  zrhval  21868  reldmdsmm  22094  frlmrcl  22118  reldmpsr  22277  reldmmpl  22350  reldmopsr  22409  reldmevls  22448  reldmmhp  22513  vr1val  22565  reldmevls1  22690  evl1fval  22701  matbas0pc  22779  mdetfval  22956  madufval  23007  qtopres  24072  fgabs  24253  reldmtng  25012  reldmnghm  25086  reldmnmhm  25087  dvbsss  26277  reldmmdeg  26430  nbgrprc0  29972  wwlksn  30483  of0r  33370  reldmrloc  33917  erlval  33918  reldmresv  33993  bj-restsnid  38278  reldmfrlm  43830  mzpmfp  44024  brovmptimex  45288  clnbgrprc0  49191  grimdmrel  49251  grlimdmrel  49351  1aryenef  50088  2aryenef  50099  resccat  50519  reldmfunc  50520  reldmoppf  50572  reldmup  50622  reldmup2  50629  reldmxpcALT  50700  fucofvalne  50778  reldmprcof  50841  reldmprcof2  50848  prcof1  50854  reldmlan  51125  reldmran  51126  reldmlan2  51131  reldmran2  51132  reldmlmd  51161  reldmcmd  51162