Theorem offinsupp1

Description: Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023)

	Ref	Expression
Hypotheses	offinsupp1.a	$$⊢\phi \to A\in V$$
	offinsupp1.y	$$⊢\phi \to Y\in U$$
	offinsupp1.z	$$⊢\phi \to Z\in W$$
	offinsupp1.f	$$⊢\phi \to F:A⟶S$$
	offinsupp1.g	$$⊢\phi \to G:A⟶T$$
	offinsupp1.1	$$⊢\phi \to {finSupp}_Y\left(F\right)$$
	offinsupp1.2	$$⊢\left(\phi \wedge x\in T\right)\to YRx=Z$$
Assertion	offinsupp1	$$⊢\phi \to {finSupp}_Z\left(\left(F{R}_{f}G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		offinsupp1.a	$$⊢\phi \to A\in V$$
2		offinsupp1.y	$$⊢\phi \to Y\in U$$
3		offinsupp1.z	$$⊢\phi \to Z\in W$$
4		offinsupp1.f	$$⊢\phi \to F:A⟶S$$
5		offinsupp1.g	$$⊢\phi \to G:A⟶T$$
6		offinsupp1.1	$$⊢\phi \to {finSupp}_Y\left(F\right)$$
7		offinsupp1.2	$$⊢\left(\phi \wedge x\in T\right)\to YRx=Z$$
8	6	fsuppimpd	$$⊢\phi \to F\mathrm{supp}Y\in \mathrm{Fin}$$
9		ssidd	$$⊢\phi \to F\mathrm{supp}Y\subseteq F\mathrm{supp}Y$$
10	9 7 4 5 1 2	suppssof1	$$⊢\phi \to \left(F{R}_{f}G\right)\mathrm{supp}Z\subseteq F\mathrm{supp}Y$$
11	8 10	ssfid	$$⊢\phi \to \left(F{R}_{f}G\right)\mathrm{supp}Z\in \mathrm{Fin}$$
12		ovexd	$$⊢\left(\phi \wedge \left(i\in S\wedge j\in T\right)\right)\to iRj\in \mathrm{V}$$
13		inidm	$$⊢A\cap A=A$$
14	12 4 5 1 1 13	off	$$⊢\phi \to \left(F{R}_{f}G\right):A⟶\mathrm{V}$$
15	14	ffund	$$⊢\phi \to \mathrm{Fun}\left(F{R}_{f}G\right)$$
16		ovexd	$$⊢\phi \to F{R}_{f}G\in \mathrm{V}$$
17		funisfsupp	$$⊢\left(\mathrm{Fun}\left(F{R}_{f}G\right)\wedge F{R}_{f}G\in \mathrm{V}\wedge Z\in W\right)\to \left({finSupp}_Z\left(\left(F{R}_{f}G\right)\right)\leftrightarrow \left(F{R}_{f}G\right)\mathrm{supp}Z\in \mathrm{Fin}\right)$$
18	15 16 3 17	syl3anc	$$⊢\phi \to \left({finSupp}_Z\left(\left(F{R}_{f}G\right)\right)\leftrightarrow \left(F{R}_{f}G\right)\mathrm{supp}Z\in \mathrm{Fin}\right)$$
19	11 18	mpbird	$$⊢\phi \to {finSupp}_Z\left(\left(F{R}_{f}G\right)\right)$$