Theorem afv2fv0

Description: If the function's value at an argument is the empty set, then the alternate function value at this argument is the empty set or undefined. (Contributed by AV, 3-Sep-2022)

	Ref	Expression
Assertion	afv2fv0	⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ → ( ( 𝐹 '''' 𝐴 ) = ∅ ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ioran	⊢ ( ¬ ( ( 𝐹 '''' 𝐴 ) = ∅ ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ↔ ( ¬ ( 𝐹 '''' 𝐴 ) = ∅ ∧ ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )
2		nnel	⊢ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
3		afv2rnfveq	⊢ ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
4	2 3	sylbi	⊢ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
5	4	eqeq1d	⊢ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) = ∅ ↔ ( 𝐹 ‘ 𝐴 ) = ∅ ) )
6	5	notbid	⊢ ( ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( ¬ ( 𝐹 '''' 𝐴 ) = ∅ ↔ ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) )
7	6	biimpac	⊢ ( ( ¬ ( 𝐹 '''' 𝐴 ) = ∅ ∧ ¬ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) → ¬ ( 𝐹 ‘ 𝐴 ) = ∅ )
8	1 7	sylbi	⊢ ( ¬ ( ( 𝐹 '''' 𝐴 ) = ∅ ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) → ¬ ( 𝐹 ‘ 𝐴 ) = ∅ )
9	8	con4i	⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ → ( ( 𝐹 '''' 𝐴 ) = ∅ ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )