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

Theorem 0mpo0 7492
Description: A mapping operation with empty domain is empty. Generalization of mpo0 7494. (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 7414 . . 3 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)}
2 df-oprab 7413 . . 3 {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)} = {𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))}
31, 2eqtri 2761 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))}
4 nel02 4333 . . . . . . . . . 10 (𝐴 = ∅ → ¬ 𝑥𝐴)
5 nel02 4333 . . . . . . . . . 10 (𝐵 = ∅ → ¬ 𝑦𝐵)
64, 5orim12i 908 . . . . . . . . 9 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (¬ 𝑥𝐴 ∨ ¬ 𝑦𝐵))
7 ianor 981 . . . . . . . . 9 (¬ (𝑥𝐴𝑦𝐵) ↔ (¬ 𝑥𝐴 ∨ ¬ 𝑦𝐵))
86, 7sylibr 233 . . . . . . . 8 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑥𝐴𝑦𝐵))
9 simprl 770 . . . . . . . 8 ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)) → (𝑥𝐴𝑦𝐵))
108, 9nsyl 140 . . . . . . 7 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1110nexdv 1940 . . . . . 6 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1211nexdv 1940 . . . . 5 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1312nexdv 1940 . . . 4 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1413alrimiv 1931 . . 3 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ∀𝑣 ¬ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
15 eqeq1 2737 . . . . . 6 (𝑧 = 𝑣 → (𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩))
1615anbi1d 631 . . . . 5 (𝑧 = 𝑣 → ((𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))))
17163exbidv 1929 . . . 4 (𝑧 = 𝑣 → (∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)) ↔ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))))
1817ab0w 4374 . . 3 ({𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))} = ∅ ↔ ∀𝑣 ¬ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1914, 18sylibr 233 . 2 ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))} = ∅)
203, 19eqtrid 2785 1 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥𝐴, 𝑦𝐵𝐶) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wo 846  wal 1540   = wceq 1542  wex 1782  wcel 2107  {cab 2710  c0 4323  cop 4635  {coprab 7410  cmpo 7411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-dif 3952  df-nul 4324  df-oprab 7413  df-mpo 7414
This theorem is referenced by:  mpo0v  7493  homffval  17634  comfffval  17642  natfval  17897  xpchomfval  18131  xpccofval  18134  plusffval  18567  efmndplusg  18761  grpsubfval  18868  grpsubfvalALT  18869  oppglsm  19510  dvrfval  20216  scaffval  20490  ipffval  21201  psrmulr  21503  marrepfval  22062  marepvfval  22067  pcofval  24526  clwwlknonmpo  29342  mendplusgfval  41927  mendmulrfval  41929  mendvscafval  41932
  Copyright terms: Public domain W3C validator