Theorem mpondm0 7661

Description: The value of an operation given by a maps-to rule is the empty set if the arguments are not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017.)

Hypothesis

Ref	Expression
mpondm0.f	⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)

Assertion

Ref	Expression
mpondm0	⊢ (¬ (𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉𝐹𝑊) = ∅)

Distinct variable groups:   𝑥,𝑦,𝑋   𝑥,𝑌,𝑦

Allowed substitution hints:   𝐶(𝑥, 𝑦)   𝐹(𝑥, 𝑦)   𝑉(𝑥, 𝑦)   𝑊(𝑥, 𝑦)

Proof of Theorem mpondm0

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpondm0.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)
2		df-mpo 7425	. . . . 5 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝑧 = 𝐶)}
3	1, 2	eqtri 2783	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝑧 = 𝐶)}
4	3	dmeqi 5885	. . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝑧 = 𝐶)}
5		dmoprabss 7524	. . 3 ⊢ dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝑧 = 𝐶)} ⊆ (𝑋 × 𝑌)
6	4, 5	eqsstri 3954	. 2 ⊢ dom 𝐹 ⊆ (𝑋 × 𝑌)
7		nssdmovg 7603	. 2 ⊢ ((dom 𝐹 ⊆ (𝑋 × 𝑌) ∧ ¬ (𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌)) → (𝑉𝐹𝑊) = ∅)
8	6, 7	mpan 703	1 ⊢ (¬ (𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉𝐹𝑊) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895  ∅c0 4278   × cxp 5648  dom cdm 5650  (class class class)co 7420  {coprab 7421   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-dm 5660  df-iota 6494  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425

This theorem is used by:  2mpo0  7670  elovmpt3imp  7678  el2mpocsbcl  8096  bropopvvv  8101  supp0prc  8180  brovex  8239  swrdnznd  14790  pfxnndmnd  14822  fullfunc  18083  fthfunc  18084  natfval  18124  evlval  22409  matbas0  22725  matrcl  22727  marrepfval  22875  marepvfval  22880  submafval  22894  minmar1fval  22961  hmeofval  24077  nghmfval  25041  wspthsn  30437  iswwlksnon  30442  iswspthsnon  30445  clwwlkn  30617  clwwlkneq0  30620  clwwlknon  30681  clwwlk0on0  30683  clwwlknon0  30684  fineqvnttrclselem1  35789  naryfval  49740  naryfvalixp  49741  oppc1stflem  50395