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

Theorem 0mpo0 7224
 Description: A mapping operation with empty domain is empty. Generalization of mpo0 7226. (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 7148 . . 3 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 df-oprab 7147 . . 3 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶))}
31, 2eqtri 2782 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶))}
4 nel02 4227 . . . . . . . . . 10 (𝐴 = ∅ → ¬ 𝑥𝐴)
5 nel02 4227 . . . . . . . . . 10 (𝐵 = ∅ → ¬ 𝑦𝐵)
64, 5orim12i 907 . . . . . . . . 9 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (¬ 𝑥𝐴 ∨ ¬ 𝑦𝐵))
7 ianor 980 . . . . . . . . 9 (¬ (𝑥𝐴𝑦𝐵) ↔ (¬ 𝑥𝐴 ∨ ¬ 𝑦𝐵))
86, 7sylibr 237 . . . . . . . 8 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑥𝐴𝑦𝐵))
9 simprl 771 . . . . . . . 8 ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)) → (𝑥𝐴𝑦𝐵))
108, 9nsyl 142 . . . . . . 7 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)))
1110nexdv 1938 . . . . . 6 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)))
1211nexdv 1938 . . . . 5 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)))
1312nexdv 1938 . . . 4 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)))
1413alrimiv 1929 . . 3 ((𝐴 = ∅ ∨ 𝐵 = ∅) → ∀𝑤 ¬ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)))
15 ab0 4266 . . 3 ({𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶))} = ∅ ↔ ∀𝑤 ¬ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)))
1614, 15sylibr 237 . 2 ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶))} = ∅)
173, 16syl5eq 2806 1 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥𝐴, 𝑦𝐵𝐶) = ∅)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∨ wo 845  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2112  {cab 2736  ∅c0 4221  ⟨cop 4521  {coprab 7144   ∈ cmpo 7145 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-dif 3857  df-nul 4222  df-oprab 7147  df-mpo 7148 This theorem is referenced by:  mpo0v  7225  homffval  17003  comfffval  17011  natfval  17260  xpchomfval  17480  xpccofval  17483  plusffval  17909  efmndplusg  18096  grpsubfval  18199  grpsubfvalALT  18200  oppglsm  18819  dvrfval  19490  scaffval  19705  ipffval  20398  psrmulr  20697  marrepfval  21245  marepvfval  21250  pcofval  23696  clwwlknonmpo  27958  mendplusgfval  40487  mendmulrfval  40489  mendvscafval  40492
 Copyright terms: Public domain W3C validator