Theorem 0mpo0 7480

Description: A mapping operation with empty domain is empty. Generalization of mpo0 7482. (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.

Step	Hyp	Ref	Expression
1		df-mpo 7402	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)}
2		df-oprab 7401	. . 3 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)} = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
3	1, 2	eqtri 2786	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
4		nel02 4292	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴)
5		nel02 4292	. . . . . . . . . 10 ⊢ (𝐵 = ∅ → ¬ 𝑦 ∈ 𝐵)
6	4, 5	orim12i 919	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵))
7		ianor 995	. . . . . . . . 9 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵))
8	6, 7	sylibr 236	. . . . . . . 8 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
9		simprl 780	. . . . . . . 8 ⊢ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
10	8, 9	nsyl 140	. . . . . . 7 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
11	10	nexdv 1957	. . . . . 6 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
12	11	nexdv 1957	. . . . 5 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
13	12	nexdv 1957	. . . 4 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
14	13	alrimiv 1948	. . 3 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
15		eqeq1 2767	. . . . . 6 ⊢ (𝑧 = 𝑣 → (𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩))
16	15	anbi1d 640	. . . . 5 ⊢ (𝑧 = 𝑣 → ((𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
17	16	3exbidv 1946	. . . 4 ⊢ (𝑧 = 𝑣 → (∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
18	17	ab0w 4333	. . 3 ⊢ ({𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅ ↔ ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
19	14, 18	sylibr 236	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅)
20	3, 19	eqtrid 2810	1 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 858  ∀wal 1559   = wceq 1561  ∃wex 1800   ∈ wcel 2143  {cab 2741  ∅c0 4286  ⟨cop 4589  {coprab 7398   ∈ cmpo 7399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3908  df-nul 4287  df-oprab 7401  df-mpo 7402

This theorem is referenced by:  mpo0v  7481  homffval  17723  comfffval  17731  natfval  17983  xpchomfval  18212  xpccofval  18215  plusffval  18681  efmndplusg  18915  grpsubfval  19026  grpsubfvalALT  19027  oppglsm  19683  dvrfval  20452  scaffval  20948  ipffval  21701  psrmulr  21995  marrepfval  22621  marepvfval  22626  pcofval  25073  clwwlknonmpo  30292  mendplusgfval  43759  mendmulrfval  43761  mendvscafval  43764  homf0  49631  upfval  49798