| Step | Hyp | Ref
| Expression |
| 1 | | suppcoss.f |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝐴) |
| 2 | | dffn3 6748 |
. . . 4
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
| 3 | 1, 2 | sylib 218 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ran 𝐹) |
| 4 | | suppcoss.g |
. . 3
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
| 5 | 3, 4 | fcod 6761 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐵⟶ran 𝐹) |
| 6 | | eldif 3961 |
. . . . 5
⊢ (𝑘 ∈ (𝐵 ∖ (𝐺 supp 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ (𝐺 supp 𝑌))) |
| 7 | 4 | ffnd 6737 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn 𝐵) |
| 8 | | suppcoss.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
| 9 | | suppcoss.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 10 | | elsuppfn 8195 |
. . . . . . . . 9
⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑊 ∧ 𝑌 ∈ 𝑉) → (𝑘 ∈ (𝐺 supp 𝑌) ↔ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌))) |
| 11 | 7, 8, 9, 10 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ (𝐺 supp 𝑌) ↔ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌))) |
| 12 | 11 | notbid 318 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝑘 ∈ (𝐺 supp 𝑌) ↔ ¬ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌))) |
| 13 | 12 | anbi2d 630 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ (𝐺 supp 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌)))) |
| 14 | | annotanannot 835 |
. . . . . 6
⊢ ((𝑘 ∈ 𝐵 ∧ ¬ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌)) |
| 15 | 13, 14 | bitrdi 287 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ (𝐺 supp 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌))) |
| 16 | 6, 15 | bitrid 283 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ (𝐵 ∖ (𝐺 supp 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌))) |
| 17 | | nne 2944 |
. . . . . 6
⊢ (¬
(𝐺‘𝑘) ≠ 𝑌 ↔ (𝐺‘𝑘) = 𝑌) |
| 18 | 17 | anbi2i 623 |
. . . . 5
⊢ ((𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌) ↔ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) |
| 19 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → 𝐺:𝐵⟶𝐴) |
| 20 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → 𝑘 ∈ 𝐵) |
| 21 | 19, 20 | fvco3d 7009 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → ((𝐹 ∘ 𝐺)‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
| 22 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → (𝐺‘𝑘) = 𝑌) |
| 23 | 22 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘𝑌)) |
| 24 | | suppcoss.1 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑌) = 𝑍) |
| 25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → (𝐹‘𝑌) = 𝑍) |
| 26 | 21, 23, 25 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍) |
| 27 | 26 | ex 412 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍)) |
| 28 | 18, 27 | biimtrid 242 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍)) |
| 29 | 16, 28 | sylbid 240 |
. . 3
⊢ (𝜑 → (𝑘 ∈ (𝐵 ∖ (𝐺 supp 𝑌)) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍)) |
| 30 | 29 | imp 406 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐺 supp 𝑌))) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍) |
| 31 | 5, 30 | suppss 8219 |
1
⊢ (𝜑 → ((𝐹 ∘ 𝐺) supp 𝑍) ⊆ (𝐺 supp 𝑌)) |