Metamath Proof Explorer

Theorem afv2ndeffv0

Description: If the alternate function value at an argument is undefined, i.e., not in the range of the function, the function's value at this argument is the empty set. (Contributed by AV, 3-Sep-2022)

		Ref	Expression
	Assertion	afv2ndeffv0	$⊢ (F'''' A) \notin ran F \to F (A) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-nel	$⊢ (F'''' A) \notin ran F \leftrightarrow \neg (F'''' A) \in ran F$
2		dfatafv2rnb	$⊢ F defAt A \leftrightarrow (F'''' A) \in ran F$
3		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
4	2 3	bitr3i	$⊢ (F'''' A) \in ran F \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
5	4	notbii	$⊢ \neg (F'''' A) \in ran F \leftrightarrow \neg (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
6		ianor	$⊢ \neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \leftrightarrow (\neg A \in dom F \lor \neg Fun ({F ↾}_{\{A\}}))$
7	1 5 6	3bitri	$⊢ (F'''' A) \notin ran F \leftrightarrow (\neg A \in dom F \lor \neg Fun ({F ↾}_{\{A\}}))$
8		ndmfv	$⊢ \neg A \in dom F \to F (A) = \emptyset$
9		nfunsn	$⊢ \neg Fun ({F ↾}_{\{A\}}) \to F (A) = \emptyset$
10	8 9	jaoi	$⊢ (\neg A \in dom F \lor \neg Fun ({F ↾}_{\{A\}})) \to F (A) = \emptyset$
11	7 10	sylbi	$⊢ (F'''' A) \notin ran F \to F (A) = \emptyset$