nssdmovg

Description: The value of an operation outside its domain. (Contributed by Alexander van der Vekens, 7-Sep-2017)

		Ref	Expression
	Assertion	nssdmovg	$⊢ (dom F \subseteq R \times S \land \neg (A \in R \land B \in S)) \to A F B = \emptyset$

Step	Hyp	Ref	Expression
1		df-ov	$⊢ A F B = F (⟨A, B⟩)$
2		ssel2	$⊢ (dom F \subseteq R \times S \land ⟨A, B⟩ \in dom F) \to ⟨A, B⟩ \in (R \times S)$
3		opelxp	$⊢ ⟨A, B⟩ \in (R \times S) \leftrightarrow (A \in R \land B \in S)$
4	2 3	sylib	$⊢ (dom F \subseteq R \times S \land ⟨A, B⟩ \in dom F) \to (A \in R \land B \in S)$
5	4	stoic1a	$⊢ (dom F \subseteq R \times S \land \neg (A \in R \land B \in S)) \to \neg ⟨A, B⟩ \in dom F$
6		ndmfv	$⊢ \neg ⟨A, B⟩ \in dom F \to F (⟨A, B⟩) = \emptyset$
7	5 6	syl	$⊢ (dom F \subseteq R \times S \land \neg (A \in R \land B \in S)) \to F (⟨A, B⟩) = \emptyset$
8	1 7	syl5eq	$⊢ (dom F \subseteq R \times S \land \neg (A \in R \land B \in S)) \to A F B = \emptyset$

Metamath Proof Explorer