Theorem mapfienlem1

Description: Lemma 1 for mapfien . (Contributed by AV, 3-Jul-2019) (Revised by AV, 28-Jul-2024)

	Ref	Expression
Hypotheses	mapfien.s	$$⊢S=\left\{x\in \left(B^A\right)|{finSupp}_Z\left(x\right)\right\}$$
	mapfien.t	$$⊢T=\left\{x\in \left(D^C\right)|{finSupp}_W\left(x\right)\right\}$$
	mapfien.w	$$⊢W=G\left(Z\right)$$
	mapfien.f	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}A$$
	mapfien.g	$$⊢\phi \to G:B\underset{1-1\; onto}{⟶}D$$
	mapfien.a	$$⊢\phi \to A\in U$$
	mapfien.b	$$⊢\phi \to B\in V$$
	mapfien.c	$$⊢\phi \to C\in X$$
	mapfien.d	$$⊢\phi \to D\in Y$$
	mapfien.z	$$⊢\phi \to Z\in B$$
Assertion	mapfienlem1	$$⊢\left(\phi \wedge f\in S\right)\to {finSupp}_W\left(\left(G\circ \left(f\circ F\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapfien.s	$$⊢S=\left\{x\in \left(B^A\right)|{finSupp}_Z\left(x\right)\right\}$$
2		mapfien.t	$$⊢T=\left\{x\in \left(D^C\right)|{finSupp}_W\left(x\right)\right\}$$
3		mapfien.w	$$⊢W=G\left(Z\right)$$
4		mapfien.f	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}A$$
5		mapfien.g	$$⊢\phi \to G:B\underset{1-1\; onto}{⟶}D$$
6		mapfien.a	$$⊢\phi \to A\in U$$
7		mapfien.b	$$⊢\phi \to B\in V$$
8		mapfien.c	$$⊢\phi \to C\in X$$
9		mapfien.d	$$⊢\phi \to D\in Y$$
10		mapfien.z	$$⊢\phi \to Z\in B$$
11	3	fvexi	$$⊢W\in \mathrm{V}$$
12	11	a1i	$$⊢\left(\phi \wedge f\in S\right)\to W\in \mathrm{V}$$
13	10	adantr	$$⊢\left(\phi \wedge f\in S\right)\to Z\in B$$
14		elrabi	$$⊢f\in \left\{x\in \left(B^A\right)|{finSupp}_Z\left(x\right)\right\}\to f\in \left(B^A\right)$$
15		elmapi	$$⊢f\in \left(B^A\right)\to f:A⟶B$$
16	14 15	syl	$$⊢f\in \left\{x\in \left(B^A\right)|{finSupp}_Z\left(x\right)\right\}\to f:A⟶B$$
17	16 1	eleq2s	$$⊢f\in S\to f:A⟶B$$
18		f1of	$$⊢F:C\underset{1-1\; onto}{⟶}A\to F:C⟶A$$
19	4 18	syl	$$⊢\phi \to F:C⟶A$$
20		fco	$$⊢\left(f:A⟶B\wedge F:C⟶A\right)\to \left(f\circ F\right):C⟶B$$
21	17 19 20	syl2anr	$$⊢\left(\phi \wedge f\in S\right)\to \left(f\circ F\right):C⟶B$$
22		f1of	$$⊢G:B\underset{1-1\; onto}{⟶}D\to G:B⟶D$$
23	5 22	syl	$$⊢\phi \to G:B⟶D$$
24	23	adantr	$$⊢\left(\phi \wedge f\in S\right)\to G:B⟶D$$
25		ssidd	$$⊢\left(\phi \wedge f\in S\right)\to B\subseteq B$$
26	8	adantr	$$⊢\left(\phi \wedge f\in S\right)\to C\in X$$
27	7	adantr	$$⊢\left(\phi \wedge f\in S\right)\to B\in V$$
28		breq1	$$⊢x=f\to \left({finSupp}_Z\left(x\right)\leftrightarrow {finSupp}_Z\left(f\right)\right)$$
29	28 1	elrab2	$$⊢f\in S\leftrightarrow \left(f\in \left(B^A\right)\wedge {finSupp}_Z\left(f\right)\right)$$
30	29	simprbi	$$⊢f\in S\to {finSupp}_Z\left(f\right)$$
31	30	adantl	$$⊢\left(\phi \wedge f\in S\right)\to {finSupp}_Z\left(f\right)$$
32		f1of1	$$⊢F:C\underset{1-1\; onto}{⟶}A\to F:C\underset{1-1}{⟶}A$$
33	4 32	syl	$$⊢\phi \to F:C\underset{1-1}{⟶}A$$
34	33	adantr	$$⊢\left(\phi \wedge f\in S\right)\to F:C\underset{1-1}{⟶}A$$
35		simpr	$$⊢\left(\phi \wedge f\in S\right)\to f\in S$$
36	31 34 13 35	fsuppco	$$⊢\left(\phi \wedge f\in S\right)\to {finSupp}_Z\left(\left(f\circ F\right)\right)$$
37	3	eqcomi	$$⊢G\left(Z\right)=W$$
38	37	a1i	$$⊢\left(\phi \wedge f\in S\right)\to G\left(Z\right)=W$$
39	12 13 21 24 25 26 27 36 38	fsuppcor	$$⊢\left(\phi \wedge f\in S\right)\to {finSupp}_W\left(\left(G\circ \left(f\circ F\right)\right)\right)$$