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	$$⊢F\left(A\right)=\varnothing \to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$

Proof

Step	Hyp	Ref	Expression
1		ioran	$$⊢\neg \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\leftrightarrow \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\varnothing \wedge \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$
2		nnel	$$⊢\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F$$
3		afv2rnfveq	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$
4	2 3	sylbi	$$⊢\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$
5	4	eqeq1d	$$⊢\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\varnothing \leftrightarrow F\left(A\right)=\varnothing \right)$$
6	5	notbid	$$⊢\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\varnothing \leftrightarrow \neg F\left(A\right)=\varnothing \right)$$
7	6	biimpac	$$⊢\left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\varnothing \wedge \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\to \neg F\left(A\right)=\varnothing$$
8	1 7	sylbi	$$⊢\neg \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\to \neg F\left(A\right)=\varnothing$$
9	8	con4i	$$⊢F\left(A\right)=\varnothing \to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$