Theorem fisuppov1

Description: Formula building theorem for finite support: operator with left annihilator. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	fisuppov1.1	$$⊢\phi \to Z\in V$$
	fisuppov1.2	$$⊢\phi \to \underset{\dot{}}{0}\in X$$
	fisuppov1.3	$$⊢\phi \to A\in W$$
	fisuppov1.4	$$⊢\phi \to D\subseteq A$$
	fisuppov1.5	$$⊢\left(\phi \wedge x\in D\right)\to B\in Y$$
	fisuppov1.6	$$⊢\phi \to F:A⟶E$$
	fisuppov1.7	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
	fisuppov1.8	$$⊢\left(\phi \wedge y\in Y\right)\to \underset{\dot{}}{0}Oy=Z$$
Assertion	fisuppov1	$$⊢\phi \to {finSupp}_Z\left(\left(x\in D⟼F\left(x\right)OB\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fisuppov1.1	$$⊢\phi \to Z\in V$$
2		fisuppov1.2	$$⊢\phi \to \underset{\dot{}}{0}\in X$$
3		fisuppov1.3	$$⊢\phi \to A\in W$$
4		fisuppov1.4	$$⊢\phi \to D\subseteq A$$
5		fisuppov1.5	$$⊢\left(\phi \wedge x\in D\right)\to B\in Y$$
6		fisuppov1.6	$$⊢\phi \to F:A⟶E$$
7		fisuppov1.7	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
8		fisuppov1.8	$$⊢\left(\phi \wedge y\in Y\right)\to \underset{\dot{}}{0}Oy=Z$$
9	3 4	ssexd	$$⊢\phi \to D\in \mathrm{V}$$
10	9	mptexd	$$⊢\phi \to \left(x\in D⟼F\left(x\right)OB\right)\in \mathrm{V}$$
11		funmpt	$$⊢\mathrm{Fun}\left(x\in D⟼F\left(x\right)OB\right)$$
12	11	a1i	$$⊢\phi \to \mathrm{Fun}\left(x\in D⟼F\left(x\right)OB\right)$$
13	6 4	feqresmpt	$$⊢\phi \to {F\upharpoonright }_D=\left(x\in D⟼F\left(x\right)\right)$$
14	13	oveq1d	$$⊢\phi \to \left({F\upharpoonright }_D\right)\mathrm{supp}\underset{\dot{}}{0}=\left(x\in D⟼F\left(x\right)\right)\mathrm{supp}\underset{\dot{}}{0}$$
15	6 3	fexd	$$⊢\phi \to F\in \mathrm{V}$$
16		ressuppss	$$⊢\left(F\in \mathrm{V}\wedge \underset{\dot{}}{0}\in X\right)\to \left({F\upharpoonright }_D\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
17	15 2 16	syl2anc	$$⊢\phi \to \left({F\upharpoonright }_D\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
18	14 17	eqsstrrd	$$⊢\phi \to \left(x\in D⟼F\left(x\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
19		fvexd	$$⊢\left(\phi \wedge x\in D\right)\to F\left(x\right)\in \mathrm{V}$$
20	18 8 19 5 2	suppssov1	$$⊢\phi \to \left(x\in D⟼F\left(x\right)OB\right)\mathrm{supp}Z\subseteq F\mathrm{supp}\underset{\dot{}}{0}$$
21	10 1 12 7 20	fsuppsssuppgd	$$⊢\phi \to {finSupp}_Z\left(\left(x\in D⟼F\left(x\right)OB\right)\right)$$