Theorem 0mpo0 7390

Description: A mapping operation with empty domain is empty. Generalization of mpo0 7392. (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 7312	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)}
2		df-oprab 7311	. . 3 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)} = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
3	1, 2	eqtri 2764	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))}
4		nel02 4272	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴)
5		nel02 4272	. . . . . . . . . 10 ⊢ (𝐵 = ∅ → ¬ 𝑦 ∈ 𝐵)
6	4, 5	orim12i 907	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵))
7		ianor 980	. . . . . . . . 9 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵))
8	6, 7	sylibr 233	. . . . . . . 8 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
9		simprl 769	. . . . . . . 8 ⊢ ((𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
10	8, 9	nsyl 140	. . . . . . 7 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
11	10	nexdv 1937	. . . . . 6 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
12	11	nexdv 1937	. . . . 5 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
13	12	nexdv 1937	. . . 4 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
14	13	alrimiv 1928	. . 3 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
15		eqeq1 2740	. . . . . 6 ⊢ (𝑧 = 𝑣 → (𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ↔ 𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩))
16	15	anbi1d 631	. . . . 5 ⊢ (𝑧 = 𝑣 → ((𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
17	16	3exbidv 1926	. . . 4 ⊢ (𝑧 = 𝑣 → (∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))))
18	17	ab0w 4313	. . 3 ⊢ ({𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅ ↔ ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))
19	14, 18	sylibr 233	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = ⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅)
20	3, 19	eqtrid 2788	1 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 845  ∀wal 1537   = wceq 1539  ∃wex 1779   ∈ wcel 2104  {cab 2713  ∅c0 4262  ⟨cop 4571  {coprab 7308   ∈ cmpo 7309

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-dif 3895  df-nul 4263  df-oprab 7311  df-mpo 7312

This theorem is referenced by:  mpo0v  7391  homffval  17448  comfffval  17456  natfval  17711  xpchomfval  17945  xpccofval  17948  plusffval  18381  efmndplusg  18568  grpsubfval  18672  grpsubfvalALT  18673  oppglsm  19296  dvrfval  19975  scaffval  20190  ipffval  20902  psrmulr  21202  marrepfval  21758  marepvfval  21763  pcofval  24222  clwwlknonmpo  28502  mendplusgfval  41206  mendmulrfval  41208  mendvscafval  41211