Theorem afvfv0bi

Description: The function's value at an argument is the empty set if and only if the value of the alternative function at this argument is either the empty set or the universe. (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afvfv0bi	$$⊢F\left(A\right)=\varnothing \leftrightarrow \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ioran	$$⊢\neg \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\right)\leftrightarrow \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \wedge \neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\right)$$
2		df-ne	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\ne \mathrm{V}\leftrightarrow \neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}$$
3		afvnufveq	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)\ne \mathrm{V}\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$
4	2 3	sylbir	$$⊢\neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)$$
5		eqeq1	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \leftrightarrow F\left(A\right)=\varnothing \right)$$
6	5	notbid	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)\to \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \leftrightarrow \neg F\left(A\right)=\varnothing \right)$$
7	6	biimpd	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=F\left(A\right)\to \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \to \neg F\left(A\right)=\varnothing \right)$$
8	4 7	syl	$$⊢\neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\to \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \to \neg F\left(A\right)=\varnothing \right)$$
9	8	impcom	$$⊢\left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \wedge \neg \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\right)\to \neg F\left(A\right)=\varnothing$$
10	1 9	sylbi	$$⊢\neg \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\right)\to \neg F\left(A\right)=\varnothing$$
11	10	con4i	$$⊢F\left(A\right)=\varnothing \to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\right)$$
12		afv0fv0	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \to F\left(A\right)=\varnothing$$
13		afvpcfv0	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\to F\left(A\right)=\varnothing$$
14	12 13	jaoi	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\right)\to F\left(A\right)=\varnothing$$
15	11 14	impbii	$$⊢F\left(A\right)=\varnothing \leftrightarrow \left(\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\varnothing \vee \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\right)$$