Step | Hyp | Ref
| Expression |
1 | | suppofssd.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
2 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) |
4 | | suppofssd.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) |
5 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐺:𝐴⟶𝐵 → 𝐺 Fn 𝐴) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn 𝐴) |
7 | | suppofssd.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
8 | | inidm 3822 |
. . . . . . 7
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
9 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
10 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) = (𝐺‘𝑦)) |
11 | 3, 6, 7, 7, 8, 9, 10 | ofval 6906 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐹 ∘𝑓 𝑋𝐺)‘𝑦) = ((𝐹‘𝑦)𝑋(𝐺‘𝑦))) |
12 | 11 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑍) → ((𝐹 ∘𝑓 𝑋𝐺)‘𝑦) = ((𝐹‘𝑦)𝑋(𝐺‘𝑦))) |
13 | | simpr 477 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑍) → (𝐹‘𝑦) = 𝑍) |
14 | 13 | oveq1d 6665 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑍) → ((𝐹‘𝑦)𝑋(𝐺‘𝑦)) = (𝑍𝑋(𝐺‘𝑦))) |
15 | | suppofss1d.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑍𝑋𝑥) = 𝑍) |
16 | 15 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑍𝑋𝑥) = 𝑍) |
17 | 16 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∀𝑥 ∈ 𝐵 (𝑍𝑋𝑥) = 𝑍) |
18 | 4 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐵) |
19 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 = (𝐺‘𝑦)) → 𝑥 = (𝐺‘𝑦)) |
20 | 19 | oveq2d 6666 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 = (𝐺‘𝑦)) → (𝑍𝑋𝑥) = (𝑍𝑋(𝐺‘𝑦))) |
21 | 20 | eqeq1d 2624 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 = (𝐺‘𝑦)) → ((𝑍𝑋𝑥) = 𝑍 ↔ (𝑍𝑋(𝐺‘𝑦)) = 𝑍)) |
22 | 18, 21 | rspcdv 3312 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (∀𝑥 ∈ 𝐵 (𝑍𝑋𝑥) = 𝑍 → (𝑍𝑋(𝐺‘𝑦)) = 𝑍)) |
23 | 17, 22 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑍𝑋(𝐺‘𝑦)) = 𝑍) |
24 | 23 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑍) → (𝑍𝑋(𝐺‘𝑦)) = 𝑍) |
25 | 12, 14, 24 | 3eqtrd 2660 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ (𝐹‘𝑦) = 𝑍) → ((𝐹 ∘𝑓 𝑋𝐺)‘𝑦) = 𝑍) |
26 | 25 | ex 450 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) = 𝑍 → ((𝐹 ∘𝑓 𝑋𝐺)‘𝑦) = 𝑍)) |
27 | 26 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ((𝐹‘𝑦) = 𝑍 → ((𝐹 ∘𝑓 𝑋𝐺)‘𝑦) = 𝑍)) |
28 | 3, 6, 7, 7, 8 | offn 6908 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 𝑋𝐺) Fn 𝐴) |
29 | | ssid 3624 |
. . . 4
⊢ 𝐴 ⊆ 𝐴 |
30 | 29 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ 𝐴) |
31 | | suppofssd.2 |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
32 | | suppfnss 7320 |
. . 3
⊢ ((((𝐹 ∘𝑓
𝑋𝐺) Fn 𝐴 ∧ 𝐹 Fn 𝐴) ∧ (𝐴 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝐵)) → (∀𝑦 ∈ 𝐴 ((𝐹‘𝑦) = 𝑍 → ((𝐹 ∘𝑓 𝑋𝐺)‘𝑦) = 𝑍) → ((𝐹 ∘𝑓 𝑋𝐺) supp 𝑍) ⊆ (𝐹 supp 𝑍))) |
33 | 28, 3, 30, 7, 31, 32 | syl23anc 1333 |
. 2
⊢ (𝜑 → (∀𝑦 ∈ 𝐴 ((𝐹‘𝑦) = 𝑍 → ((𝐹 ∘𝑓 𝑋𝐺)‘𝑦) = 𝑍) → ((𝐹 ∘𝑓 𝑋𝐺) supp 𝑍) ⊆ (𝐹 supp 𝑍))) |
34 | 27, 33 | mpd 15 |
1
⊢ (𝜑 → ((𝐹 ∘𝑓 𝑋𝐺) supp 𝑍) ⊆ (𝐹 supp 𝑍)) |