Proof of Theorem fsuppun
Step | Hyp | Ref
| Expression |
1 | | cnvun 6006 |
. . . . . . 7
⊢ ◡(𝐹 ∪ 𝐺) = (◡𝐹 ∪ ◡𝐺) |
2 | 1 | imaeq1i 5926 |
. . . . . 6
⊢ (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍})) = ((◡𝐹 ∪ ◡𝐺) “ (V ∖ {𝑍})) |
3 | | imaundir 6014 |
. . . . . 6
⊢ ((◡𝐹 ∪ ◡𝐺) “ (V ∖ {𝑍})) = ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐺 “ (V ∖ {𝑍}))) |
4 | 2, 3 | eqtri 2765 |
. . . . 5
⊢ (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍})) = ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐺 “ (V ∖ {𝑍}))) |
5 | | unexb 7533 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ↔ (𝐹 ∪ 𝐺) ∈ V) |
6 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → 𝐹 ∈ V) |
7 | 5, 6 | sylbir 238 |
. . . . . . . . . 10
⊢ ((𝐹 ∪ 𝐺) ∈ V → 𝐹 ∈ V) |
8 | | suppimacnv 7916 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
9 | 7, 8 | sylan 583 |
. . . . . . . . 9
⊢ (((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
10 | 9 | eqcomd 2743 |
. . . . . . . 8
⊢ (((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → (◡𝐹 “ (V ∖ {𝑍})) = (𝐹 supp 𝑍)) |
11 | 10 | adantr 484 |
. . . . . . 7
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (◡𝐹 “ (V ∖ {𝑍})) = (𝐹 supp 𝑍)) |
12 | | fsuppun.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 finSupp 𝑍) |
13 | 12 | fsuppimpd 8992 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
14 | 13 | adantl 485 |
. . . . . . 7
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (𝐹 supp 𝑍) ∈ Fin) |
15 | 11, 14 | eqeltrd 2838 |
. . . . . 6
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (◡𝐹 “ (V ∖ {𝑍})) ∈ Fin) |
16 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → 𝐺 ∈ V) |
17 | 5, 16 | sylbir 238 |
. . . . . . . . 9
⊢ ((𝐹 ∪ 𝐺) ∈ V → 𝐺 ∈ V) |
18 | | suppimacnv 7916 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ V ∧ 𝑍 ∈ V) → (𝐺 supp 𝑍) = (◡𝐺 “ (V ∖ {𝑍}))) |
19 | 18 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝑍 ∈ V) → (◡𝐺 “ (V ∖ {𝑍})) = (𝐺 supp 𝑍)) |
20 | 17, 19 | sylan 583 |
. . . . . . . 8
⊢ (((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → (◡𝐺 “ (V ∖ {𝑍})) = (𝐺 supp 𝑍)) |
21 | 20 | adantr 484 |
. . . . . . 7
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (◡𝐺 “ (V ∖ {𝑍})) = (𝐺 supp 𝑍)) |
22 | | fsuppun.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 finSupp 𝑍) |
23 | 22 | fsuppimpd 8992 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 supp 𝑍) ∈ Fin) |
24 | 23 | adantl 485 |
. . . . . . 7
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (𝐺 supp 𝑍) ∈ Fin) |
25 | 21, 24 | eqeltrd 2838 |
. . . . . 6
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (◡𝐺 “ (V ∖ {𝑍})) ∈ Fin) |
26 | | unfi 8850 |
. . . . . 6
⊢ (((◡𝐹 “ (V ∖ {𝑍})) ∈ Fin ∧ (◡𝐺 “ (V ∖ {𝑍})) ∈ Fin) → ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐺 “ (V ∖ {𝑍}))) ∈ Fin) |
27 | 15, 25, 26 | syl2anc 587 |
. . . . 5
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((◡𝐹 “ (V ∖ {𝑍})) ∪ (◡𝐺 “ (V ∖ {𝑍}))) ∈ Fin) |
28 | 4, 27 | eqeltrid 2842 |
. . . 4
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍})) ∈ Fin) |
29 | | suppimacnv 7916 |
. . . . . 6
⊢ (((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) supp 𝑍) = (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍}))) |
30 | 29 | eleq1d 2822 |
. . . . 5
⊢ (((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → (((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin ↔ (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍})) ∈ Fin)) |
31 | 30 | adantr 484 |
. . . 4
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin ↔ (◡(𝐹 ∪ 𝐺) “ (V ∖ {𝑍})) ∈ Fin)) |
32 | 28, 31 | mpbird 260 |
. . 3
⊢ ((((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
33 | 32 | ex 416 |
. 2
⊢ (((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin)) |
34 | | supp0prc 7906 |
. . . 4
⊢ (¬
((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) supp 𝑍) = ∅) |
35 | | 0fin 8849 |
. . . 4
⊢ ∅
∈ Fin |
36 | 34, 35 | eqeltrdi 2846 |
. . 3
⊢ (¬
((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
37 | 36 | a1d 25 |
. 2
⊢ (¬
((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → (𝜑 → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin)) |
38 | 33, 37 | pm2.61i 185 |
1
⊢ (𝜑 → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |