Proof of Theorem fsuppunbi
Step | Hyp | Ref
| Expression |
1 | | relfsupp 8160 |
. . . . 5
⊢ Rel
finSupp |
2 | | brrelex12 5079 |
. . . . 5
⊢ ((Rel
finSupp ∧ (𝐹 ∪
𝐺) finSupp 𝑍) → ((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V)) |
3 | 1, 2 | mpan 702 |
. . . 4
⊢ ((𝐹 ∪ 𝐺) finSupp 𝑍 → ((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V)) |
4 | | unexb 6856 |
. . . . 5
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ↔ (𝐹 ∪ 𝐺) ∈ V) |
5 | | fsuppimp 8164 |
. . . . . . 7
⊢ ((𝐹 ∪ 𝐺) finSupp 𝑍 → (Fun (𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin)) |
6 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
7 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
8 | | simprlr 799 |
. . . . . . . . . . . . 13
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐺 ∈ V) |
9 | 8 | suppun 7202 |
. . . . . . . . . . . 12
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) |
10 | | ssfi 8065 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin ∧ (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) → (𝐹 supp 𝑍) ∈ Fin) |
11 | 7, 9, 10 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 supp 𝑍) ∈ Fin) |
12 | | fununfun 5848 |
. . . . . . . . . . . . . . 15
⊢ (Fun
(𝐹 ∪ 𝐺) → (Fun 𝐹 ∧ Fun 𝐺)) |
13 | 12 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ (Fun
(𝐹 ∪ 𝐺) → Fun 𝐹) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → Fun 𝐹) |
15 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → Fun 𝐹) |
16 | | simprll 798 |
. . . . . . . . . . . 12
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐹 ∈ V) |
17 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → 𝑍 ∈ V) |
18 | 17 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝑍 ∈ V) |
19 | | funisfsupp 8163 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 finSupp 𝑍 ↔ (𝐹 supp 𝑍) ∈ Fin)) |
20 | 15, 16, 18, 19 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 finSupp 𝑍 ↔ (𝐹 supp 𝑍) ∈ Fin)) |
21 | 11, 20 | mpbird 246 |
. . . . . . . . . 10
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐹 finSupp 𝑍) |
22 | | uncom 3719 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∪ 𝐺) = (𝐺 ∪ 𝐹) |
23 | 22 | oveq1i 6559 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∪ 𝐺) supp 𝑍) = ((𝐺 ∪ 𝐹) supp 𝑍) |
24 | 23 | eleq1i 2679 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin ↔ ((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin) |
25 | 24 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin → ((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → ((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin) |
27 | 26 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → ((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin) |
28 | 16 | suppun 7202 |
. . . . . . . . . . . 12
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐺 supp 𝑍) ⊆ ((𝐺 ∪ 𝐹) supp 𝑍)) |
29 | | ssfi 8065 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ ((𝐺 ∪ 𝐹) supp 𝑍)) → (𝐺 supp 𝑍) ∈ Fin) |
30 | 27, 28, 29 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐺 supp 𝑍) ∈ Fin) |
31 | 12 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (Fun
(𝐹 ∪ 𝐺) → Fun 𝐺) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → Fun 𝐺) |
33 | 32 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → Fun 𝐺) |
34 | | funisfsupp 8163 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐺 ∧ 𝐺 ∈ V ∧ 𝑍 ∈ V) → (𝐺 finSupp 𝑍 ↔ (𝐺 supp 𝑍) ∈ Fin)) |
35 | 33, 8, 18, 34 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐺 finSupp 𝑍 ↔ (𝐺 supp 𝑍) ∈ Fin)) |
36 | 30, 35 | mpbird 246 |
. . . . . . . . . 10
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐺 finSupp 𝑍) |
37 | 21, 36 | jca 553 |
. . . . . . . . 9
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) |
38 | 37 | a1d 25 |
. . . . . . . 8
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍))) |
39 | 38 | ex 449 |
. . . . . . 7
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)))) |
40 | 5, 39 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∪ 𝐺) finSupp 𝑍 → (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)))) |
41 | 40 | com12 32 |
. . . . 5
⊢ (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) finSupp 𝑍 → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)))) |
42 | 4, 41 | sylanbr 489 |
. . . 4
⊢ (((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) finSupp 𝑍 → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)))) |
43 | 3, 42 | mpcom 37 |
. . 3
⊢ ((𝐹 ∪ 𝐺) finSupp 𝑍 → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍))) |
44 | 43 | com12 32 |
. 2
⊢ (𝜑 → ((𝐹 ∪ 𝐺) finSupp 𝑍 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍))) |
45 | | simpl 472 |
. . . . . 6
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → 𝐹 finSupp 𝑍) |
46 | | simpr 476 |
. . . . . 6
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → 𝐺 finSupp 𝑍) |
47 | 45, 46 | fsuppun 8177 |
. . . . 5
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
48 | 47 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
49 | | fsuppunbi.u |
. . . . . 6
⊢ (𝜑 → Fun (𝐹 ∪ 𝐺)) |
50 | 49 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → Fun (𝐹 ∪ 𝐺)) |
51 | 1 | brrelexi 5082 |
. . . . . . 7
⊢ (𝐹 finSupp 𝑍 → 𝐹 ∈ V) |
52 | 1 | brrelexi 5082 |
. . . . . . 7
⊢ (𝐺 finSupp 𝑍 → 𝐺 ∈ V) |
53 | | unexg 6857 |
. . . . . . 7
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 ∪ 𝐺) ∈ V) |
54 | 51, 52, 53 | syl2an 493 |
. . . . . 6
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → (𝐹 ∪ 𝐺) ∈ V) |
55 | 54 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → (𝐹 ∪ 𝐺) ∈ V) |
56 | 1 | brrelex2i 5083 |
. . . . . . 7
⊢ (𝐹 finSupp 𝑍 → 𝑍 ∈ V) |
57 | 56 | adantr 480 |
. . . . . 6
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → 𝑍 ∈ V) |
58 | 57 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → 𝑍 ∈ V) |
59 | | funisfsupp 8163 |
. . . . 5
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ (𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) finSupp 𝑍 ↔ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin)) |
60 | 50, 55, 58, 59 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → ((𝐹 ∪ 𝐺) finSupp 𝑍 ↔ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin)) |
61 | 48, 60 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → (𝐹 ∪ 𝐺) finSupp 𝑍) |
62 | 61 | ex 449 |
. 2
⊢ (𝜑 → ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → (𝐹 ∪ 𝐺) finSupp 𝑍)) |
63 | 44, 62 | impbid 201 |
1
⊢ (𝜑 → ((𝐹 ∪ 𝐺) finSupp 𝑍 ↔ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍))) |