MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpt2ndm0 Structured version   Visualization version   GIF version

Theorem mpt2ndm0 6647
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
mpt2ndm0.f 𝐹 = (𝑥𝑋, 𝑦𝑌𝐶)
Assertion
Ref Expression
mpt2ndm0 (¬ (𝑉𝑋𝑊𝑌) → (𝑉𝐹𝑊) = ∅)
Distinct variable groups:   𝑥,𝑦,𝑋   𝑥,𝑌,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem mpt2ndm0
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 mpt2ndm0.f . . . . 5 𝐹 = (𝑥𝑋, 𝑦𝑌𝐶)
2 df-mpt2 6430 . . . . 5 (𝑥𝑋, 𝑦𝑌𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝑋𝑦𝑌) ∧ 𝑧 = 𝐶)}
31, 2eqtri 2536 . . . 4 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝑋𝑦𝑌) ∧ 𝑧 = 𝐶)}
43dmeqi 5138 . . 3 dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝑋𝑦𝑌) ∧ 𝑧 = 𝐶)}
5 dmoprabss 6515 . . 3 dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝑋𝑦𝑌) ∧ 𝑧 = 𝐶)} ⊆ (𝑋 × 𝑌)
64, 5eqsstri 3502 . 2 dom 𝐹 ⊆ (𝑋 × 𝑌)
7 nssdmovg 6588 . 2 ((dom 𝐹 ⊆ (𝑋 × 𝑌) ∧ ¬ (𝑉𝑋𝑊𝑌)) → (𝑉𝐹𝑊) = ∅)
86, 7mpan 701 1 (¬ (𝑉𝑋𝑊𝑌) → (𝑉𝐹𝑊) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1474  wcel 1938  wss 3444  c0 3777   × cxp 4930  dom cdm 4932  (class class class)co 6425  {coprab 6426  cmpt2 6427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-xp 4938  df-dm 4942  df-iota 5653  df-fv 5697  df-ov 6428  df-oprab 6429  df-mpt2 6430
This theorem is referenced by:  2mpt20  6654  elovmpt3imp  6662  el2mpt2csbcl  7010  bropopvvv  7015  supp0prc  7058  brovex  7108  fullfunc  16285  fthfunc  16286  natfval  16325  evlval  19253  matbas0  19942  matrcl  19944  marrepfval  20092  marepvfval  20097  submafval  20111  minmar1fval  20178  hmeofval  21278  nghmfval  22233  nghmfvalOLD  22251  uvtxisvtx  25767  uvtx0  25768  uvtx01vtx  25769  clwwlknprop  26049  2wlkonot3v  26151  2spthonot3v  26152  wspthsn  41137  iswwlksnon  41142  iswspthsnon  41143  wspn0  41222  av-numclwwlkffin0  41604
  Copyright terms: Public domain W3C validator