This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑆 ⟶ 𝐵 ) → ( 𝑥 ∈ 𝐼 ↦ 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 bitrid ⊢ ( 𝜑 → ( 𝐹 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( 𝑓 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 } ↔ ( 𝐹 : 𝑆 ⟶ 𝐵 ∧ ( 𝐹 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )