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 ) e/ ran F -> ( F ` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-nel	|- ( ( F '''' A ) e/ ran F <-> -. ( F '''' A ) e. ran F )
2		dfatafv2rnb	|- ( F defAt A <-> ( F '''' A ) e. ran F )
3		df-dfat	|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
4	2 3	bitr3i	|- ( ( F '''' A ) e. ran F <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
5	4	notbii	|- ( -. ( F '''' A ) e. ran F <-> -. ( A e. dom F /\ Fun ( F |` { A } ) ) )
6		ianor	|- ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) <-> ( -. A e. dom F \/ -. Fun ( F |` { A } ) ) )
7	1 5 6	3bitri	|- ( ( F '''' A ) e/ ran F <-> ( -. A e. dom F \/ -. Fun ( F |` { A } ) ) )
8		ndmfv	|- ( -. A e. dom F -> ( F ` A ) = (/) )
9		nfunsn	|- ( -. Fun ( F |` { A } ) -> ( F ` A ) = (/) )
10	8 9	jaoi	|- ( ( -. A e. dom F \/ -. Fun ( F |` { A } ) ) -> ( F ` A ) = (/) )
11	7 10	sylbi	|- ( ( F '''' A ) e/ ran F -> ( F ` A ) = (/) )