Metamath Proof Explorer

Theorem mpondm0

Description: The value of an operation given by a maps-to rule is the empty set if the arguments are not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017)

		Ref	Expression
	Hypothesis	mpondm0.f	$⊢ F = (x \in X, y \in Y ⟼ C)$
	Assertion	mpondm0	$⊢ \neg (V \in X \land W \in Y) \to V F W = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		mpondm0.f	$⊢ F = (x \in X, y \in Y ⟼ C)$
2		df-mpo	$⊢ (x \in X, y \in Y ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in X \land y \in Y) \land z = C)\}$
3	1 2	eqtri	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in X \land y \in Y) \land z = C)\}$
4	3	dmeqi	$⊢ dom F = dom \{⟨⟨x, y⟩, z⟩ \| ((x \in X \land y \in Y) \land z = C)\}$
5		dmoprabss	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| ((x \in X \land y \in Y) \land z = C)\} \subseteq X \times Y$
6	4 5	eqsstri	$⊢ dom F \subseteq X \times Y$
7		nssdmovg	$⊢ (dom F \subseteq X \times Y \land \neg (V \in X \land W \in Y)) \to V F W = \emptyset$
8	6 7	mpan	$⊢ \neg (V \in X \land W \in Y) \to V F W = \emptyset$