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

Theorem 0mpo0 7516
Description: A mapping operation with empty domain is empty. Generalization of mpo0 7518. (Contributed by AV, 27-Jan-2024.)
Assertion
Ref Expression
0mpo0 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥𝐴, 𝑦𝐵𝐶) = ∅)
Distinct variable groups:   𝑦,𝐴   𝑥,𝐴   𝑥,𝐵   𝑦,𝐵
Allowed substitution hints:   𝐶(𝑥,𝑦)

Proof of Theorem 0mpo0
Dummy variables 𝑤 𝑧 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-mpo 7436 . . 3 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)}
2 df-oprab 7435 . . 3 {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)} = {𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))}
31, 2eqtri 2765 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))}
4 nel02 4339 . . . . . . . . . 10 (𝐴 = ∅ → ¬ 𝑥𝐴)
5 nel02 4339 . . . . . . . . . 10 (𝐵 = ∅ → ¬ 𝑦𝐵)
64, 5orim12i 909 . . . . . . . . 9 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (¬ 𝑥𝐴 ∨ ¬ 𝑦𝐵))
7 ianor 984 . . . . . . . . 9 (¬ (𝑥𝐴𝑦𝐵) ↔ (¬ 𝑥𝐴 ∨ ¬ 𝑦𝐵))
86, 7sylibr 234 . . . . . . . 8 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑥𝐴𝑦𝐵))
9 simprl 771 . . . . . . . 8 ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)) → (𝑥𝐴𝑦𝐵))
108, 9nsyl 140 . . . . . . 7 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1110nexdv 1936 . . . . . 6 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1211nexdv 1936 . . . . 5 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1312nexdv 1936 . . . 4 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1413alrimiv 1927 . . 3 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ∀𝑣 ¬ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
15 eqeq1 2741 . . . . . 6 (𝑧 = 𝑣 → (𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩))
1615anbi1d 631 . . . . 5 (𝑧 = 𝑣 → ((𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))))
17163exbidv 1925 . . . 4 (𝑧 = 𝑣 → (∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)) ↔ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))))
1817ab0w 4379 . . 3 ({𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))} = ∅ ↔ ∀𝑣 ¬ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1914, 18sylibr 234 . 2 ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))} = ∅)
203, 19eqtrid 2789 1 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥𝐴, 𝑦𝐵𝐶) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848  wal 1538   = wceq 1540  wex 1779  wcel 2108  {cab 2714  c0 4333  cop 4632  {coprab 7432  cmpo 7433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-dif 3954  df-nul 4334  df-oprab 7435  df-mpo 7436
This theorem is referenced by:  mpo0v  7517  homffval  17733  comfffval  17741  natfval  17994  xpchomfval  18224  xpccofval  18227  plusffval  18659  efmndplusg  18893  grpsubfval  19001  grpsubfvalALT  19002  oppglsm  19660  dvrfval  20402  scaffval  20878  ipffval  21666  psrmulr  21962  marrepfval  22566  marepvfval  22571  pcofval  25043  clwwlknonmpo  30108  mendplusgfval  43193  mendmulrfval  43195  mendvscafval  43198  upfval  48933
  Copyright terms: Public domain W3C validator