0mpo0

Description: A mapping operation with empty domain is empty. Generalization of mpo0 . (Contributed by AV, 27-Jan-2024)

		Ref	Expression
	Assertion	0mpo0	$⊢ (A = \emptyset \lor B = \emptyset) \to (x \in A, y \in B ⟼ C) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, w⟩ \| ((x \in A \land y \in B) \land w = C)\}$
2		df-oprab	$⊢ \{⟨⟨x, y⟩, w⟩ \| ((x \in A \land y \in B) \land w = C)\} = \{z \| \exists x \exists y \exists w (z = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))\}$
3	1 2	eqtri	$⊢ (x \in A, y \in B ⟼ C) = \{z \| \exists x \exists y \exists w (z = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))\}$
4		nel02	$⊢ A = \emptyset \to \neg x \in A$
5		nel02	$⊢ B = \emptyset \to \neg y \in B$
6	4 5	orim12i	$⊢ (A = \emptyset \lor B = \emptyset) \to (\neg x \in A \lor \neg y \in B)$
7		ianor	$⊢ \neg (x \in A \land y \in B) \leftrightarrow (\neg x \in A \lor \neg y \in B)$
8	6 7	sylibr	$⊢ (A = \emptyset \lor B = \emptyset) \to \neg (x \in A \land y \in B)$
9		simprl	$⊢ (v = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C)) \to (x \in A \land y \in B)$
10	8 9	nsyl	$⊢ (A = \emptyset \lor B = \emptyset) \to \neg (v = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))$
11	10	nexdv	$⊢ (A = \emptyset \lor B = \emptyset) \to \neg \exists w (v = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))$
12	11	nexdv	$⊢ (A = \emptyset \lor B = \emptyset) \to \neg \exists y \exists w (v = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))$
13	12	nexdv	$⊢ (A = \emptyset \lor B = \emptyset) \to \neg \exists x \exists y \exists w (v = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))$
14	13	alrimiv	$⊢ (A = \emptyset \lor B = \emptyset) \to \forall v \neg \exists x \exists y \exists w (v = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))$
15		eqeq1	$⊢ z = v \to (z = ⟨⟨x, y⟩, w⟩ \leftrightarrow v = ⟨⟨x, y⟩, w⟩)$
16	15	anbi1d	$⊢ z = v \to ((z = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C)) \leftrightarrow (v = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C)))$
17	16	3exbidv	$⊢ z = v \to (\exists x \exists y \exists w (z = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C)) \leftrightarrow \exists x \exists y \exists w (v = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C)))$
18	17	ab0w	$⊢ \{z \| \exists x \exists y \exists w (z = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))\} = \emptyset \leftrightarrow \forall v \neg \exists x \exists y \exists w (v = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))$
19	14 18	sylibr	$⊢ (A = \emptyset \lor B = \emptyset) \to \{z \| \exists x \exists y \exists w (z = ⟨⟨x, y⟩, w⟩ \land ((x \in A \land y \in B) \land w = C))\} = \emptyset$
20	3 19	eqtrid	$⊢ (A = \emptyset \lor B = \emptyset) \to (x \in A, y \in B ⟼ C) = \emptyset$

Metamath Proof Explorer

Theorem 0mpo0

Proof