Theorem gsumcllem

Description: Lemma for gsumcl and related theorems. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 31-May-2019)

	Ref	Expression
Hypotheses	gsumcllem.f	$$⊢\phi \to F:A⟶B$$
	gsumcllem.a	$$⊢\phi \to A\in V$$
	gsumcllem.z	$$⊢\phi \to Z\in U$$
	gsumcllem.s	$$⊢\phi \to F\mathrm{supp}Z\subseteq W$$
Assertion	gsumcllem	$$⊢\left(\phi \wedge W=\varnothing \right)\to F=\left(k\in A⟼Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumcllem.f	$$⊢\phi \to F:A⟶B$$
2		gsumcllem.a	$$⊢\phi \to A\in V$$
3		gsumcllem.z	$$⊢\phi \to Z\in U$$
4		gsumcllem.s	$$⊢\phi \to F\mathrm{supp}Z\subseteq W$$
5	1	feqmptd	$$⊢\phi \to F=\left(k\in A⟼F\left(k\right)\right)$$
6	5	adantr	$$⊢\left(\phi \wedge W=\varnothing \right)\to F=\left(k\in A⟼F\left(k\right)\right)$$
7		difeq2	$$⊢W=\varnothing \to A\setminus W=A\setminus \varnothing$$
8		dif0	$$⊢A\setminus \varnothing =A$$
9	7 8	syl6eq	$$⊢W=\varnothing \to A\setminus W=A$$
10	9	eleq2d	$$⊢W=\varnothing \to \left(k\in \left(A\setminus W\right)\leftrightarrow k\in A\right)$$
11	10	biimpar	$$⊢\left(W=\varnothing \wedge k\in A\right)\to k\in \left(A\setminus W\right)$$
12	1 4 2 3	suppssr	$$⊢\left(\phi \wedge k\in \left(A\setminus W\right)\right)\to F\left(k\right)=Z$$
13	11 12	sylan2	$$⊢\left(\phi \wedge \left(W=\varnothing \wedge k\in A\right)\right)\to F\left(k\right)=Z$$
14	13	anassrs	$$⊢\left(\left(\phi \wedge W=\varnothing \right)\wedge k\in A\right)\to F\left(k\right)=Z$$
15	14	mpteq2dva	$$⊢\left(\phi \wedge W=\varnothing \right)\to \left(k\in A⟼F\left(k\right)\right)=\left(k\in A⟼Z\right)$$
16	6 15	eqtrd	$$⊢\left(\phi \wedge W=\varnothing \right)\to F=\left(k\in A⟼Z\right)$$