Proof of Theorem imacosuppOLD
Step | Hyp | Ref
| Expression |
1 | | cnvco 5756 |
. . . . . . . 8
⊢ ◡(𝐹 ∘ 𝐺) = (◡𝐺 ∘ ◡𝐹) |
2 | 1 | imaeq1i 5926 |
. . . . . . 7
⊢ (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})) = ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍})) |
3 | | imaco 6104 |
. . . . . . 7
⊢ ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍})) = (◡𝐺 “ (◡𝐹 “ (V ∖ {𝑍}))) |
4 | 2, 3 | eqtri 2844 |
. . . . . 6
⊢ (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})) = (◡𝐺 “ (◡𝐹 “ (V ∖ {𝑍}))) |
5 | 4 | imaeq2i 5927 |
. . . . 5
⊢ (𝐺 “ (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍}))) = (𝐺 “ (◡𝐺 “ (◡𝐹 “ (V ∖ {𝑍})))) |
6 | | funforn 6597 |
. . . . . . . 8
⊢ (Fun
𝐺 ↔ 𝐺:dom 𝐺–onto→ran 𝐺) |
7 | 6 | biimpi 218 |
. . . . . . 7
⊢ (Fun
𝐺 → 𝐺:dom 𝐺–onto→ran 𝐺) |
8 | 7 | ad2antrl 726 |
. . . . . 6
⊢ (((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) ∧ (Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺)) → 𝐺:dom 𝐺–onto→ran 𝐺) |
9 | | simpl 485 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → 𝐹 ∈ 𝑉) |
10 | 9 | anim2i 618 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝑍 ∈ V ∧ 𝐹 ∈ 𝑉)) |
11 | 10 | ancomd 464 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝐹 ∈ 𝑉 ∧ 𝑍 ∈ V)) |
12 | | suppimacnv 7841 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
14 | 13 | sseq1d 3998 |
. . . . . . . . 9
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((𝐹 supp 𝑍) ⊆ ran 𝐺 ↔ (◡𝐹 “ (V ∖ {𝑍})) ⊆ ran 𝐺)) |
15 | 14 | biimpd 231 |
. . . . . . . 8
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((𝐹 supp 𝑍) ⊆ ran 𝐺 → (◡𝐹 “ (V ∖ {𝑍})) ⊆ ran 𝐺)) |
16 | 15 | adantld 493 |
. . . . . . 7
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (◡𝐹 “ (V ∖ {𝑍})) ⊆ ran 𝐺)) |
17 | 16 | imp 409 |
. . . . . 6
⊢ (((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) ∧ (Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺)) → (◡𝐹 “ (V ∖ {𝑍})) ⊆ ran 𝐺) |
18 | | foimacnv 6632 |
. . . . . 6
⊢ ((𝐺:dom 𝐺–onto→ran 𝐺 ∧ (◡𝐹 “ (V ∖ {𝑍})) ⊆ ran 𝐺) → (𝐺 “ (◡𝐺 “ (◡𝐹 “ (V ∖ {𝑍})))) = (◡𝐹 “ (V ∖ {𝑍}))) |
19 | 8, 17, 18 | syl2anc 586 |
. . . . 5
⊢ (((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) ∧ (Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺)) → (𝐺 “ (◡𝐺 “ (◡𝐹 “ (V ∖ {𝑍})))) = (◡𝐹 “ (V ∖ {𝑍}))) |
20 | 5, 19 | syl5eq 2868 |
. . . 4
⊢ (((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) ∧ (Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺)) → (𝐺 “ (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍}))) = (◡𝐹 “ (V ∖ {𝑍}))) |
21 | | coexg 7634 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘ 𝐺) ∈ V) |
22 | 21 | anim2i 618 |
. . . . . . . 8
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝑍 ∈ V ∧ (𝐹 ∘ 𝐺) ∈ V)) |
23 | 22 | ancomd 464 |
. . . . . . 7
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V)) |
24 | | suppimacnv 7841 |
. . . . . . 7
⊢ (((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍}))) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍}))) |
26 | 25 | imaeq2d 5929 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐺 “ (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})))) |
27 | 26 | adantr 483 |
. . . 4
⊢ (((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) ∧ (Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺)) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐺 “ (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})))) |
28 | 13 | adantr 483 |
. . . 4
⊢ (((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) ∧ (Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺)) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
29 | 20, 27, 28 | 3eqtr4d 2866 |
. . 3
⊢ (((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) ∧ (Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺)) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍)) |
30 | 29 | exp31 422 |
. 2
⊢ (𝑍 ∈ V → ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍)))) |
31 | | ima0 5945 |
. . . 4
⊢ (𝐺 “ ∅) =
∅ |
32 | | id 22 |
. . . . . . 7
⊢ (¬
𝑍 ∈ V → ¬
𝑍 ∈
V) |
33 | 32 | intnand 491 |
. . . . . 6
⊢ (¬
𝑍 ∈ V → ¬
((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V)) |
34 | | supp0prc 7833 |
. . . . . 6
⊢ (¬
((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅) |
35 | 33, 34 | syl 17 |
. . . . 5
⊢ (¬
𝑍 ∈ V → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅) |
36 | 35 | imaeq2d 5929 |
. . . 4
⊢ (¬
𝑍 ∈ V → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐺 “ ∅)) |
37 | 32 | intnand 491 |
. . . . 5
⊢ (¬
𝑍 ∈ V → ¬
(𝐹 ∈ V ∧ 𝑍 ∈ V)) |
38 | | supp0prc 7833 |
. . . . 5
⊢ (¬
(𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅) |
39 | 37, 38 | syl 17 |
. . . 4
⊢ (¬
𝑍 ∈ V → (𝐹 supp 𝑍) = ∅) |
40 | 31, 36, 39 | 3eqtr4a 2882 |
. . 3
⊢ (¬
𝑍 ∈ V → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍)) |
41 | 40 | 2a1d 26 |
. 2
⊢ (¬
𝑍 ∈ V → ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍)))) |
42 | 30, 41 | pm2.61i 184 |
1
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍))) |