Metamath Proof Explorer

Theorem 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⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
2		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C))\}$
3	1 2	eqtri	$⊢ (x \in A, y \in B ⟼ C) = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = 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	$⊢ (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C)) \to (x \in A \land y \in B)$
10	8 9	nsyl	$⊢ (A = \emptyset \lor B = \emptyset) \to \neg (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C))$
11	10	nexdv	$⊢ (A = \emptyset \lor B = \emptyset) \to \neg \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C))$
12	11	nexdv	$⊢ (A = \emptyset \lor B = \emptyset) \to \neg \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C))$
13	12	nexdv	$⊢ (A = \emptyset \lor B = \emptyset) \to \neg \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C))$
14	13	alrimiv	$⊢ (A = \emptyset \lor B = \emptyset) \to \forall w \neg \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C))$
15		ab0	$⊢ \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C))\} = \emptyset \leftrightarrow \forall w \neg \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C))$
16	14 15	sylibr	$⊢ (A = \emptyset \lor B = \emptyset) \to \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ((x \in A \land y \in B) \land z = C))\} = \emptyset$
17	3 16	syl5eq	$⊢ (A = \emptyset \lor B = \emptyset) \to (x \in A, y \in B ⟼ C) = \emptyset$