Proof of Theorem fsuppssindlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq1 6905 | . . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) | 
| 2 | 1 | ifeq1d 4545 | . . . . 5
⊢ (𝑓 = 𝐹 → if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 ) = if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) | 
| 3 | 2 | mpteq2dv 5244 | . . . 4
⊢ (𝑓 = 𝐹 → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 ))) | 
| 4 | 3 | eleq1d 2826 | . . 3
⊢ (𝑓 = 𝐹 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) ∈ 𝐻)) | 
| 5 | 4 | elrab 3692 | . 2
⊢ (𝐹 ∈ {𝑓 ∈ (𝐵 ↑m 𝑆) ∣ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) ∈ 𝐻} ↔ (𝐹 ∈ (𝐵 ↑m 𝑆) ∧ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) ∈ 𝐻)) | 
| 6 |  | fsuppssindlem2.b | . . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑊) | 
| 7 |  | fsuppssindlem2.v | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 8 |  | fsuppssindlem2.s | . . . . . 6
⊢ (𝜑 → 𝑆 ⊆ 𝐼) | 
| 9 | 7, 8 | ssexd 5324 | . . . . 5
⊢ (𝜑 → 𝑆 ∈ V) | 
| 10 | 6, 9 | elmapd 8880 | . . . 4
⊢ (𝜑 → (𝐹 ∈ (𝐵 ↑m 𝑆) ↔ 𝐹:𝑆⟶𝐵)) | 
| 11 | 10 | anbi1d 631 | . . 3
⊢ (𝜑 → ((𝐹 ∈ (𝐵 ↑m 𝑆) ∧ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) ∈ 𝐻) ↔ (𝐹:𝑆⟶𝐵 ∧ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) ∈ 𝐻))) | 
| 12 |  | partfun 6715 | . . . . . 6
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) = ((𝑥 ∈ (𝐼 ∩ 𝑆) ↦ (𝐹‘𝑥)) ∪ (𝑥 ∈ (𝐼 ∖ 𝑆) ↦ 0 )) | 
| 13 |  | sseqin2 4223 | . . . . . . . . . . 11
⊢ (𝑆 ⊆ 𝐼 ↔ (𝐼 ∩ 𝑆) = 𝑆) | 
| 14 | 8, 13 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 → (𝐼 ∩ 𝑆) = 𝑆) | 
| 15 | 14 | mpteq1d 5237 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐼 ∩ 𝑆) ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝑆 ↦ (𝐹‘𝑥))) | 
| 16 | 15 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑆⟶𝐵) → (𝑥 ∈ (𝐼 ∩ 𝑆) ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝑆 ↦ (𝐹‘𝑥))) | 
| 17 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑆⟶𝐵) → 𝐹:𝑆⟶𝐵) | 
| 18 | 17 | feqmptd 6977 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑆⟶𝐵) → 𝐹 = (𝑥 ∈ 𝑆 ↦ (𝐹‘𝑥))) | 
| 19 | 16, 18 | eqtr4d 2780 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝑆⟶𝐵) → (𝑥 ∈ (𝐼 ∩ 𝑆) ↦ (𝐹‘𝑥)) = 𝐹) | 
| 20 |  | fconstmpt 5747 | . . . . . . . . 9
⊢ ((𝐼 ∖ 𝑆) × { 0 }) = (𝑥 ∈ (𝐼 ∖ 𝑆) ↦ 0 ) | 
| 21 | 20 | eqcomi 2746 | . . . . . . . 8
⊢ (𝑥 ∈ (𝐼 ∖ 𝑆) ↦ 0 ) = ((𝐼 ∖ 𝑆) × { 0 }) | 
| 22 | 21 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝑆⟶𝐵) → (𝑥 ∈ (𝐼 ∖ 𝑆) ↦ 0 ) = ((𝐼 ∖ 𝑆) × { 0 })) | 
| 23 | 19, 22 | uneq12d 4169 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝑆⟶𝐵) → ((𝑥 ∈ (𝐼 ∩ 𝑆) ↦ (𝐹‘𝑥)) ∪ (𝑥 ∈ (𝐼 ∖ 𝑆) ↦ 0 )) = (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 }))) | 
| 24 | 12, 23 | eqtrid 2789 | . . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑆⟶𝐵) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) = (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 }))) | 
| 25 | 24 | eleq1d 2826 | . . . 4
⊢ ((𝜑 ∧ 𝐹:𝑆⟶𝐵) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) ∈ 𝐻 ↔ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻)) | 
| 26 | 25 | pm5.32da 579 | . . 3
⊢ (𝜑 → ((𝐹:𝑆⟶𝐵 ∧ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) ∈ 𝐻) ↔ (𝐹:𝑆⟶𝐵 ∧ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻))) | 
| 27 | 11, 26 | bitrd 279 | . 2
⊢ (𝜑 → ((𝐹 ∈ (𝐵 ↑m 𝑆) ∧ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝐹‘𝑥), 0 )) ∈ 𝐻) ↔ (𝐹:𝑆⟶𝐵 ∧ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻))) | 
| 28 | 5, 27 | bitrid 283 | 1
⊢ (𝜑 → (𝐹 ∈ {𝑓 ∈ (𝐵 ↑m 𝑆) ∣ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) ∈ 𝐻} ↔ (𝐹:𝑆⟶𝐵 ∧ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻))) |