Theorem 0mpo0 7490

Description: A mapping operation with empty domain is empty. Generalization of mpo0 7492. (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 7410	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)}
2		df-oprab 7409	. . 3 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)} = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
3	1, 2	eqtri 2758	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
4		nel02 4314	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴)
5		nel02 4314	. . . . . . . . . 10 ⊢ (𝐵 = ∅ → ¬ 𝑦 ∈ 𝐵)
6	4, 5	orim12i 908	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵))
7		ianor 983	. . . . . . . . 9 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵))
8	6, 7	sylibr 234	. . . . . . . 8 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
9		simprl 770	. . . . . . . 8 ⊢ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
10	8, 9	nsyl 140	. . . . . . 7 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
11	10	nexdv 1936	. . . . . 6 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
12	11	nexdv 1936	. . . . 5 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
13	12	nexdv 1936	. . . 4 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
14	13	alrimiv 1927	. . 3 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
15		eqeq1 2739	. . . . . 6 ⊢ (𝑧 = 𝑣 → (𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩))
16	15	anbi1d 631	. . . . 5 ⊢ (𝑧 = 𝑣 → ((𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
17	16	3exbidv 1925	. . . 4 ⊢ (𝑧 = 𝑣 → (∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
18	17	ab0w 4354	. . 3 ⊢ ({𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅ ↔ ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
19	14, 18	sylibr 234	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅)
20	3, 19	eqtrid 2782	1 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  {cab 2713  ∅c0 4308  ⟨cop 4607  {coprab 7406   ∈ cmpo 7407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-dif 3929  df-nul 4309  df-oprab 7409  df-mpo 7410

This theorem is referenced by:  mpo0v  7491  homffval  17702  comfffval  17710  natfval  17962  xpchomfval  18191  xpccofval  18194  plusffval  18624  efmndplusg  18858  grpsubfval  18966  grpsubfvalALT  18967  oppglsm  19623  dvrfval  20362  scaffval  20837  ipffval  21608  psrmulr  21902  marrepfval  22498  marepvfval  22503  pcofval  24961  clwwlknonmpo  30070  mendplusgfval  43205  mendmulrfval  43207  mendvscafval  43210  homf0  48984  upfval  49111