Theorem fsuppssindlem2

Description: Lemma for fsuppssind . Write a function as a union. (Contributed by SN, 15-Jul-2024)

	Ref	Expression
Hypotheses	fsuppssindlem2.b	$$⊢\phi \to B\in W$$
	fsuppssindlem2.v	$$⊢\phi \to I\in V$$
	fsuppssindlem2.s	$$⊢\phi \to S\subseteq I$$
Assertion	fsuppssindlem2	$$⊢\phi \to \left(F\in \left\{f\in \left(B^S\right)|\left(x\in I⟼if\left(x\in S,f\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\right\}\leftrightarrow \left(F:S⟶B\wedge F\cup \left(\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}\right)\in H\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsuppssindlem2.b	$$⊢\phi \to B\in W$$
2		fsuppssindlem2.v	$$⊢\phi \to I\in V$$
3		fsuppssindlem2.s	$$⊢\phi \to S\subseteq I$$
4		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
5	4	ifeq1d	$$⊢f=F\to if\left(x\in S,f\left(x\right),\underset{\dot{}}{0}\right)=if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)$$
6	5	mpteq2dv	$$⊢f=F\to \left(x\in I⟼if\left(x\in S,f\left(x\right),\underset{\dot{}}{0}\right)\right)=\left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)$$
7	6	eleq1d	$$⊢f=F\to \left(\left(x\in I⟼if\left(x\in S,f\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\leftrightarrow \left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\right)$$
8	7	elrab	$$⊢F\in \left\{f\in \left(B^S\right)|\left(x\in I⟼if\left(x\in S,f\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\right\}\leftrightarrow \left(F\in \left(B^S\right)\wedge \left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\right)$$
9	2 3	ssexd	$$⊢\phi \to S\in \mathrm{V}$$
10	1 9	elmapd	$$⊢\phi \to \left(F\in \left(B^S\right)\leftrightarrow F:S⟶B\right)$$
11	10	anbi1d	$$⊢\phi \to \left(\left(F\in \left(B^S\right)\wedge \left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\right)\leftrightarrow \left(F:S⟶B\wedge \left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\right)\right)$$
12		partfun	$$⊢\left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)=\left(x\in \left(I\cap S\right)⟼F\left(x\right)\right)\cup \left(x\in \left(I\setminus S\right)⟼\underset{\dot{}}{0}\right)$$
13		sseqin2	$$⊢S\subseteq I\leftrightarrow I\cap S=S$$
14	3 13	sylib	$$⊢\phi \to I\cap S=S$$
15	14	mpteq1d	$$⊢\phi \to \left(x\in \left(I\cap S\right)⟼F\left(x\right)\right)=\left(x\in S⟼F\left(x\right)\right)$$
16	15	adantr	$$⊢\left(\phi \wedge F:S⟶B\right)\to \left(x\in \left(I\cap S\right)⟼F\left(x\right)\right)=\left(x\in S⟼F\left(x\right)\right)$$
17		simpr	$$⊢\left(\phi \wedge F:S⟶B\right)\to F:S⟶B$$
18	17	feqmptd	$$⊢\left(\phi \wedge F:S⟶B\right)\to F=\left(x\in S⟼F\left(x\right)\right)$$
19	16 18	eqtr4d	$$⊢\left(\phi \wedge F:S⟶B\right)\to \left(x\in \left(I\cap S\right)⟼F\left(x\right)\right)=F$$
20		fconstmpt	$$⊢\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}=\left(x\in \left(I\setminus S\right)⟼\underset{\dot{}}{0}\right)$$
21	20	eqcomi	$$⊢\left(x\in \left(I\setminus S\right)⟼\underset{\dot{}}{0}\right)=\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}$$
22	21	a1i	$$⊢\left(\phi \wedge F:S⟶B\right)\to \left(x\in \left(I\setminus S\right)⟼\underset{\dot{}}{0}\right)=\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}$$
23	19 22	uneq12d	$$⊢\left(\phi \wedge F:S⟶B\right)\to \left(x\in \left(I\cap S\right)⟼F\left(x\right)\right)\cup \left(x\in \left(I\setminus S\right)⟼\underset{\dot{}}{0}\right)=F\cup \left(\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}\right)$$
24	12 23	syl5eq	$$⊢\left(\phi \wedge F:S⟶B\right)\to \left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)=F\cup \left(\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}\right)$$
25	24	eleq1d	$$⊢\left(\phi \wedge F:S⟶B\right)\to \left(\left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\leftrightarrow F\cup \left(\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}\right)\in H\right)$$
26	25	pm5.32da	$$⊢\phi \to \left(\left(F:S⟶B\wedge \left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\right)\leftrightarrow \left(F:S⟶B\wedge F\cup \left(\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}\right)\in H\right)\right)$$
27	11 26	bitrd	$$⊢\phi \to \left(\left(F\in \left(B^S\right)\wedge \left(x\in I⟼if\left(x\in S,F\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\right)\leftrightarrow \left(F:S⟶B\wedge F\cup \left(\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}\right)\in H\right)\right)$$
28	8 27	syl5bb	$$⊢\phi \to \left(F\in \left\{f\in \left(B^S\right)|\left(x\in I⟼if\left(x\in S,f\left(x\right),\underset{\dot{}}{0}\right)\right)\in H\right\}\leftrightarrow \left(F:S⟶B\wedge F\cup \left(\left(I\setminus S\right)\times \left\{\underset{\dot{}}{0}\right\}\right)\in H\right)\right)$$