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 2763 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))}
4 nel02 4345 . . . . . . . . . 10 (𝐴 = ∅ → ¬ 𝑥𝐴)
5 nel02 4345 . . . . . . . . . 10 (𝐵 = ∅ → ¬ 𝑦𝐵)
64, 5orim12i 908 . . . . . . . . 9 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (¬ 𝑥𝐴 ∨ ¬ 𝑦𝐵))
7 ianor 983 . . . . . . . . 9 (¬ (𝑥𝐴𝑦𝐵) ↔ (¬ 𝑥𝐴 ∨ ¬ 𝑦𝐵))
86, 7sylibr 234 . . . . . . . 8 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑥𝐴𝑦𝐵))
9 simprl 771 . . . . . . . 8 ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)) → (𝑥𝐴𝑦𝐵))
108, 9nsyl 140 . . . . . . 7 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1110nexdv 1934 . . . . . 6 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1211nexdv 1934 . . . . 5 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1312nexdv 1934 . . . 4 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1413alrimiv 1925 . . 3 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ∀𝑣 ¬ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
15 eqeq1 2739 . . . . . 6 (𝑧 = 𝑣 → (𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩))
1615anbi1d 631 . . . . 5 (𝑧 = 𝑣 → ((𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))))
17163exbidv 1923 . . . 4 (𝑧 = 𝑣 → (∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)) ↔ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))))
1817ab0w 4385 . . 3 ({𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))} = ∅ ↔ ∀𝑣 ¬ ∃𝑥𝑦𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶)))
1914, 18sylibr 234 . 2 ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑧 ∣ ∃𝑥𝑦𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑤 = 𝐶))} = ∅)
203, 19eqtrid 2787 1 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥𝐴, 𝑦𝐵𝐶) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847  wal 1535   = wceq 1537  wex 1776  wcel 2106  {cab 2712  c0 4339  cop 4637  {coprab 7432  cmpo 7433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-dif 3966  df-nul 4340  df-oprab 7435  df-mpo 7436
This theorem is referenced by:  mpo0v  7517  homffval  17735  comfffval  17743  natfval  18001  xpchomfval  18235  xpccofval  18238  plusffval  18672  efmndplusg  18906  grpsubfval  19014  grpsubfvalALT  19015  oppglsm  19675  dvrfval  20419  scaffval  20895  ipffval  21684  psrmulr  21980  marrepfval  22582  marepvfval  22587  pcofval  25057  clwwlknonmpo  30118  mendplusgfval  43170  mendmulrfval  43172  mendvscafval  43175
  Copyright terms: Public domain W3C validator