Theorem 0mpo0 7497

Description: A mapping operation with empty domain is empty. Generalization of mpo0 7499. (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 7419	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)}
2		df-oprab 7418	. . 3 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)} = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
3	1, 2	eqtri 2783	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
4		nel02 4285	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴)
5		nel02 4285	. . . . . . . . . 10 ⊢ (𝐵 = ∅ → ¬ 𝑦 ∈ 𝐵)
6	4, 5	orim12i 922	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵))
7		ianor 997	. . . . . . . . 9 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵))
8	6, 7	sylibr 237	. . . . . . . 8 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
9		simprl 783	. . . . . . . 8 ⊢ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
10	8, 9	nsyl 141	. . . . . . 7 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
11	10	nexdv 1969	. . . . . 6 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
12	11	nexdv 1969	. . . . 5 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
13	12	nexdv 1969	. . . 4 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
14	13	alrimiv 1960	. . 3 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
15		eqeq1 2764	. . . . . 6 ⊢ (𝑧 = 𝑣 → (𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩))
16	15	anbi1d 643	. . . . 5 ⊢ (𝑧 = 𝑣 → ((𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
17	16	3exbidv 1958	. . . 4 ⊢ (𝑧 = 𝑣 → (∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
18	17	ab0w 4328	. . 3 ⊢ ({𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅ ↔ ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
19	14, 18	sylibr 237	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅)
20	3, 19	eqtrid 2807	1 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2738  ∅c0 4279  ⟨cop 4590  {coprab 7415   ∈ cmpo 7416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 3902  df-nul 4280  df-oprab 7418  df-mpo 7419

This theorem is used by:  mpo0v  7498  homffval  17781  comfffval  17789  natfval  18041  xpchomfval  18270  xpccofval  18273  plusffval  18739  efmndplusg  18992  grpsubfval  19110  grpsubfvalALT  19111  oppglsm  19772  dvrfval  20546  scaffval  21067  ipffval  21864  psrmulr  22160  marrepfval  22785  marepvfval  22790  pcofval  25241  clwwlknonmpo  30562  mendplusgfval  44025  mendmulrfval  44027  mendvscafval  44030  homf0  49938  upfval  50105