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	⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ¬ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
2		dfatafv2rnb	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
3		df-dfat	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
4	2 3	bitr3i	⊢ ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
5	4	notbii	⊢ ( ¬ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
6		ianor	⊢ ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ↔ ( ¬ 𝐴 ∈ dom 𝐹 ∨ ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
7	1 5 6	3bitri	⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ( ¬ 𝐴 ∈ dom 𝐹 ∨ ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
8		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
9		nfunsn	⊢ ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
10	8 9	jaoi	⊢ ( ( ¬ 𝐴 ∈ dom 𝐹 ∨ ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
11	7 10	sylbi	⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )