Theorem afvpcfv0

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

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

Proof

Step	Hyp	Ref	Expression
1		dfafv2	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)$$
2	1	eqeq1i	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\leftrightarrow if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)=\mathrm{V}$$
3		eqcom	$$⊢if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)=\mathrm{V}\leftrightarrow \mathrm{V}=if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)$$
4		eqif	$$⊢\mathrm{V}=if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)\leftrightarrow \left(\left(F\mathrm{defAt}A\wedge \mathrm{V}=F\left(A\right)\right)\vee \left(\neg F\mathrm{defAt}A\wedge \mathrm{V}=\mathrm{V}\right)\right)$$
5	3 4	bitri	$$⊢if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)=\mathrm{V}\leftrightarrow \left(\left(F\mathrm{defAt}A\wedge \mathrm{V}=F\left(A\right)\right)\vee \left(\neg F\mathrm{defAt}A\wedge \mathrm{V}=\mathrm{V}\right)\right)$$
6		fveqvfvv	$$⊢F\left(A\right)=\mathrm{V}\to F\left(A\right)=\varnothing$$
7	6	eqcoms	$$⊢\mathrm{V}=F\left(A\right)\to F\left(A\right)=\varnothing$$
8	7	adantl	$$⊢\left(F\mathrm{defAt}A\wedge \mathrm{V}=F\left(A\right)\right)\to F\left(A\right)=\varnothing$$
9		fvfundmfvn0	$$⊢F\left(A\right)\ne \varnothing \to \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
10		df-dfat	$$⊢F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
11	9 10	sylibr	$$⊢F\left(A\right)\ne \varnothing \to F\mathrm{defAt}A$$
12	11	necon1bi	$$⊢\neg F\mathrm{defAt}A\to F\left(A\right)=\varnothing$$
13	12	adantr	$$⊢\left(\neg F\mathrm{defAt}A\wedge \mathrm{V}=\mathrm{V}\right)\to F\left(A\right)=\varnothing$$
14	8 13	jaoi	$$⊢\left(\left(F\mathrm{defAt}A\wedge \mathrm{V}=F\left(A\right)\right)\vee \left(\neg F\mathrm{defAt}A\wedge \mathrm{V}=\mathrm{V}\right)\right)\to F\left(A\right)=\varnothing$$
15	5 14	sylbi	$$⊢if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)=\mathrm{V}\to F\left(A\right)=\varnothing$$
16	2 15	sylbi	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\mathrm{V}\to F\left(A\right)=\varnothing$$