Step | Hyp | Ref
| Expression |
1 | | suppcoss.f |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝐴) |
2 | | dffn3 6503 |
. . . 4
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
3 | 1, 2 | sylib 221 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ran 𝐹) |
4 | | suppcoss.g |
. . 3
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
5 | 3, 4 | fcod 6510 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐵⟶ran 𝐹) |
6 | | eldif 3864 |
. . . . 5
⊢ (𝑘 ∈ (𝐵 ∖ (𝐺 supp 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ (𝐺 supp 𝑌))) |
7 | 4 | ffnd 6492 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn 𝐵) |
8 | | suppcoss.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
9 | | suppcoss.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
10 | | elsuppfn 7838 |
. . . . . . . . 9
⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑊 ∧ 𝑌 ∈ 𝑉) → (𝑘 ∈ (𝐺 supp 𝑌) ↔ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌))) |
11 | 7, 8, 9, 10 | syl3anc 1369 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ (𝐺 supp 𝑌) ↔ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌))) |
12 | 11 | notbid 322 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝑘 ∈ (𝐺 supp 𝑌) ↔ ¬ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌))) |
13 | 12 | anbi2d 632 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ (𝐺 supp 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌)))) |
14 | | annotanannot 834 |
. . . . . 6
⊢ ((𝑘 ∈ 𝐵 ∧ ¬ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) ≠ 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌)) |
15 | 13, 14 | bitrdi 290 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ (𝐺 supp 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌))) |
16 | 6, 15 | syl5bb 286 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ (𝐵 ∖ (𝐺 supp 𝑌)) ↔ (𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌))) |
17 | | nne 2953 |
. . . . . 6
⊢ (¬
(𝐺‘𝑘) ≠ 𝑌 ↔ (𝐺‘𝑘) = 𝑌) |
18 | 17 | anbi2i 626 |
. . . . 5
⊢ ((𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌) ↔ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) |
19 | 4 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → 𝐺:𝐵⟶𝐴) |
20 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → 𝑘 ∈ 𝐵) |
21 | 19, 20 | fvco3d 6745 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → ((𝐹 ∘ 𝐺)‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
22 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → (𝐺‘𝑘) = 𝑌) |
23 | 22 | fveq2d 6655 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘𝑌)) |
24 | | suppcoss.1 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑌) = 𝑍) |
25 | 24 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → (𝐹‘𝑌) = 𝑍) |
26 | 21, 23, 25 | 3eqtrd 2798 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌)) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍) |
27 | 26 | ex 417 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ 𝐵 ∧ (𝐺‘𝑘) = 𝑌) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍)) |
28 | 18, 27 | syl5bi 245 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ 𝐵 ∧ ¬ (𝐺‘𝑘) ≠ 𝑌) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍)) |
29 | 16, 28 | sylbid 243 |
. . 3
⊢ (𝜑 → (𝑘 ∈ (𝐵 ∖ (𝐺 supp 𝑌)) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍)) |
30 | 29 | imp 411 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐺 supp 𝑌))) → ((𝐹 ∘ 𝐺)‘𝑘) = 𝑍) |
31 | 5, 30 | suppss 7861 |
1
⊢ (𝜑 → ((𝐹 ∘ 𝐺) supp 𝑍) ⊆ (𝐺 supp 𝑌)) |