Theorem fsuppcolem

Description: Lemma for fsuppco . Formula building theorem for finite supports: rearranging the index set. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	fsuppcolem.f	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}$$
	fsuppcolem.g	$$⊢\phi \to G:X\underset{1-1}{⟶}Y$$
Assertion	fsuppcolem	$$⊢\phi \to {\left(F\circ G\right)}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		fsuppcolem.f	$$⊢\phi \to F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}$$
2		fsuppcolem.g	$$⊢\phi \to G:X\underset{1-1}{⟶}Y$$
3		cnvco	$$⊢{\left(F\circ G\right)}^{-1}=G^{-1}\circ F^{-1}$$
4	3	imaeq1i	$$⊢{\left(F\circ G\right)}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]=\left(G^{-1}\circ F^{-1}\right)\left[\mathrm{V}\setminus \left\{Z\right\}\right]$$
5		imaco	$$⊢\left(G^{-1}\circ F^{-1}\right)\left[\mathrm{V}\setminus \left\{Z\right\}\right]=G^{-1}\left[F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\right]$$
6	4 5	eqtri	$$⊢{\left(F\circ G\right)}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]=G^{-1}\left[F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\right]$$
7		df-f1	$$⊢G:X\underset{1-1}{⟶}Y\leftrightarrow \left(G:X⟶Y\wedge \mathrm{Fun}{G}^{-1}\right)$$
8	7	simprbi	$$⊢G:X\underset{1-1}{⟶}Y\to \mathrm{Fun}{G}^{-1}$$
9	2 8	syl	$$⊢\phi \to \mathrm{Fun}{G}^{-1}$$
10		imafi	$$⊢\left(\mathrm{Fun}{G}^{-1}\wedge F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}\right)\to G^{-1}\left[F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\right]\in \mathrm{Fin}$$
11	9 1 10	syl2anc	$$⊢\phi \to G^{-1}\left[F^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\right]\in \mathrm{Fin}$$
12	6 11	eqeltrid	$$⊢\phi \to {\left(F\circ G\right)}^{-1}\left[\mathrm{V}\setminus \left\{Z\right\}\right]\in \mathrm{Fin}$$