Theorem 0mpo0 7502

Description: A mapping operation with empty domain is empty. Generalization of mpo0 7504. (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 7424	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)}
2		df-oprab 7423	. . 3 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)} = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
3	1, 2	eqtri 2788	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
4		nel02 4292	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴)
5		nel02 4292	. . . . . . . . . 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 2769	. . . . . 6 ⊢ (𝑧 = 𝑣 → (𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩))
16	15	anbi1d 643	. . . . 5 ⊢ (𝑧 = 𝑣 → ((𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
17	16	3exbidv 1958	. . . 4 ⊢ (𝑧 = 𝑣 → (∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
18	17	ab0w 4335	. . 3 ⊢ ({𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅ ↔ ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
19	14, 18	sylibr 237	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅)
20	3, 19	eqtrid 2812	1 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146  {cab 2743  ∅c0 4286  ⟨cop 4597  {coprab 7420   ∈ cmpo 7421

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-dif 3909  df-nul 4287  df-oprab 7423  df-mpo 7424

This theorem is used by:  mpo0v  7503  homffval  17770  comfffval  17778  natfval  18030  xpchomfval  18259  xpccofval  18262  plusffval  18728  efmndplusg  18978  grpsubfval  19096  grpsubfvalALT  19097  oppglsm  19758  dvrfval  20532  scaffval  21053  ipffval  21850  psrmulr  22144  marrepfval  22769  marepvfval  22774  pcofval  25222  clwwlknonmpo  30509  mendplusgfval  43968  mendmulrfval  43970  mendvscafval  43973  homf0  49846  upfval  50013