Theorem fsuppssindlem2

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

	Ref	Expression
Hypotheses	fsuppssindlem2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	fsuppssindlem2.v	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	fsuppssindlem2.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐼 )
Assertion	fsuppssindlem2	⊢ ( 𝜑 → ( 𝐹 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 } ↔ ( 𝐹 : 𝑆 ⟶ 𝐵 ∧ ( 𝐹 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fsuppssindlem2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
2		fsuppssindlem2.v	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		fsuppssindlem2.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐼 )
4		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
5	4	ifeq1d	⊢ ( 𝑓 = 𝐹 → if ( 𝑥 ∈ 𝑆 , ( 𝑓 ‘ 𝑥 ) , 0 ) = if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
6	5	mpteq2dv	⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝑓 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
7	6	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ↔ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) )
8	7	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 } ↔ ( 𝐹 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) )
9	2 3	ssexd	⊢ ( 𝜑 → 𝑆 ∈ V )
10	1 9	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐵 ↑m 𝑆 ) ↔ 𝐹 : 𝑆 ⟶ 𝐵 ) )
11	10	anbi1d	⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) ↔ ( 𝐹 : 𝑆 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) ) )
12		partfun	⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( ( 𝑥 ∈ ( 𝐼 ∩ 𝑆 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∪ ( 𝑥 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 ) )
13		sseqin2	⊢ ( 𝑆 ⊆ 𝐼 ↔ ( 𝐼 ∩ 𝑆 ) = 𝑆 )
14	3 13	sylib	⊢ ( 𝜑 → ( 𝐼 ∩ 𝑆 ) = 𝑆 )
15	14	mpteq1d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐼 ∩ 𝑆 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝐹 ‘ 𝑥 ) ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑆 ⟶ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ∩ 𝑆 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝐹 ‘ 𝑥 ) ) )
17		simpr	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑆 ⟶ 𝐵 ) → 𝐹 : 𝑆 ⟶ 𝐵 )
18	17	feqmptd	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑆 ⟶ 𝐵 ) → 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( 𝐹 ‘ 𝑥 ) ) )
19	16 18	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑆 ⟶ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ∩ 𝑆 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = 𝐹 )
20		fconstmpt	⊢ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) = ( 𝑥 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 )
21	20	eqcomi	⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 ) = ( ( 𝐼 ∖ 𝑆 ) × { 0 } )
22	21	a1i	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑆 ⟶ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 ) = ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) )
23	19 22	uneq12d	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑆 ⟶ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ∩ 𝑆 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∪ ( 𝑥 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 ) ) = ( 𝐹 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) )
24	12 23	syl5eq	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑆 ⟶ 𝐵 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝐹 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) )
25	24	eleq1d	⊢ ( ( 𝜑 ∧ 𝐹 : 𝑆 ⟶ 𝐵 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ↔ ( 𝐹 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) )
26	25	pm5.32da	⊢ ( 𝜑 → ( ( 𝐹 : 𝑆 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) ↔ ( 𝐹 : 𝑆 ⟶ 𝐵 ∧ ( 𝐹 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )
27	11 26	bitrd	⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝐵 ↑m 𝑆 ) ∧ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) ↔ ( 𝐹 : 𝑆 ⟶ 𝐵 ∧ ( 𝐹 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )
28	8 27	syl5bb	⊢ ( 𝜑 → ( 𝐹 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 } ↔ ( 𝐹 : 𝑆 ⟶ 𝐵 ∧ ( 𝐹 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )