Proof of Theorem fsuppunbi
Step | Hyp | Ref
| Expression |
1 | | relfsupp 8546 |
. . . . 5
⊢ Rel
finSupp |
2 | 1 | brrelex12i 5392 |
. . . 4
⊢ ((𝐹 ∪ 𝐺) finSupp 𝑍 → ((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V)) |
3 | | unexb 7218 |
. . . . 5
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ↔ (𝐹 ∪ 𝐺) ∈ V) |
4 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
5 | 4 | adantr 474 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
6 | | simprlr 800 |
. . . . . . . . . . . 12
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐺 ∈ V) |
7 | 6 | suppun 7579 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) |
8 | | ssfi 8449 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin ∧ (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) → (𝐹 supp 𝑍) ∈ Fin) |
9 | 5, 7, 8 | syl2anc 581 |
. . . . . . . . . 10
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 supp 𝑍) ∈ Fin) |
10 | | fununfun 6170 |
. . . . . . . . . . . . . 14
⊢ (Fun
(𝐹 ∪ 𝐺) → (Fun 𝐹 ∧ Fun 𝐺)) |
11 | 10 | simpld 490 |
. . . . . . . . . . . . 13
⊢ (Fun
(𝐹 ∪ 𝐺) → Fun 𝐹) |
12 | 11 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → Fun 𝐹) |
13 | 12 | adantr 474 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → Fun 𝐹) |
14 | | simprll 799 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐹 ∈ V) |
15 | | simpr 479 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → 𝑍 ∈ V) |
16 | 15 | adantl 475 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝑍 ∈ V) |
17 | | funisfsupp 8549 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 finSupp 𝑍 ↔ (𝐹 supp 𝑍) ∈ Fin)) |
18 | 13, 14, 16, 17 | syl3anc 1496 |
. . . . . . . . . 10
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 finSupp 𝑍 ↔ (𝐹 supp 𝑍) ∈ Fin)) |
19 | 9, 18 | mpbird 249 |
. . . . . . . . 9
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐹 finSupp 𝑍) |
20 | | uncom 3984 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∪ 𝐺) = (𝐺 ∪ 𝐹) |
21 | 20 | oveq1i 6915 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∪ 𝐺) supp 𝑍) = ((𝐺 ∪ 𝐹) supp 𝑍) |
22 | 21 | eleq1i 2897 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin ↔ ((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin) |
23 | 22 | biimpi 208 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin → ((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin) |
24 | 23 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → ((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin) |
25 | 24 | adantr 474 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → ((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin) |
26 | 14 | suppun 7579 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐺 supp 𝑍) ⊆ ((𝐺 ∪ 𝐹) supp 𝑍)) |
27 | | ssfi 8449 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∪ 𝐹) supp 𝑍) ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ ((𝐺 ∪ 𝐹) supp 𝑍)) → (𝐺 supp 𝑍) ∈ Fin) |
28 | 25, 26, 27 | syl2anc 581 |
. . . . . . . . . 10
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐺 supp 𝑍) ∈ Fin) |
29 | 10 | simprd 491 |
. . . . . . . . . . . . 13
⊢ (Fun
(𝐹 ∪ 𝐺) → Fun 𝐺) |
30 | 29 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → Fun 𝐺) |
31 | 30 | adantr 474 |
. . . . . . . . . . 11
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → Fun 𝐺) |
32 | | funisfsupp 8549 |
. . . . . . . . . . 11
⊢ ((Fun
𝐺 ∧ 𝐺 ∈ V ∧ 𝑍 ∈ V) → (𝐺 finSupp 𝑍 ↔ (𝐺 supp 𝑍) ∈ Fin)) |
33 | 31, 6, 16, 32 | syl3anc 1496 |
. . . . . . . . . 10
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐺 finSupp 𝑍 ↔ (𝐺 supp 𝑍) ∈ Fin)) |
34 | 28, 33 | mpbird 249 |
. . . . . . . . 9
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → 𝐺 finSupp 𝑍) |
35 | 19, 34 | jca 509 |
. . . . . . . 8
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) |
36 | 35 | a1d 25 |
. . . . . . 7
⊢ (((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) ∧ ((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V)) → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍))) |
37 | 36 | ex 403 |
. . . . . 6
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) → (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)))) |
38 | | fsuppimp 8550 |
. . . . . 6
⊢ ((𝐹 ∪ 𝐺) finSupp 𝑍 → (Fun (𝐹 ∪ 𝐺) ∧ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin)) |
39 | 37, 38 | syl11 33 |
. . . . 5
⊢ (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) finSupp 𝑍 → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)))) |
40 | 3, 39 | sylanbr 579 |
. . . 4
⊢ (((𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) finSupp 𝑍 → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)))) |
41 | 2, 40 | mpcom 38 |
. . 3
⊢ ((𝐹 ∪ 𝐺) finSupp 𝑍 → (𝜑 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍))) |
42 | 41 | com12 32 |
. 2
⊢ (𝜑 → ((𝐹 ∪ 𝐺) finSupp 𝑍 → (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍))) |
43 | | simpl 476 |
. . . . . 6
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → 𝐹 finSupp 𝑍) |
44 | | simpr 479 |
. . . . . 6
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → 𝐺 finSupp 𝑍) |
45 | 43, 44 | fsuppun 8563 |
. . . . 5
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
46 | 45 | adantl 475 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) |
47 | | fsuppunbi.u |
. . . . . 6
⊢ (𝜑 → Fun (𝐹 ∪ 𝐺)) |
48 | 47 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → Fun (𝐹 ∪ 𝐺)) |
49 | 1 | brrelex1i 5393 |
. . . . . . 7
⊢ (𝐹 finSupp 𝑍 → 𝐹 ∈ V) |
50 | 1 | brrelex1i 5393 |
. . . . . . 7
⊢ (𝐺 finSupp 𝑍 → 𝐺 ∈ V) |
51 | | unexg 7219 |
. . . . . . 7
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 ∪ 𝐺) ∈ V) |
52 | 49, 50, 51 | syl2an 591 |
. . . . . 6
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → (𝐹 ∪ 𝐺) ∈ V) |
53 | 52 | adantl 475 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → (𝐹 ∪ 𝐺) ∈ V) |
54 | 1 | brrelex2i 5394 |
. . . . . . 7
⊢ (𝐹 finSupp 𝑍 → 𝑍 ∈ V) |
55 | 54 | adantr 474 |
. . . . . 6
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → 𝑍 ∈ V) |
56 | 55 | adantl 475 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → 𝑍 ∈ V) |
57 | | funisfsupp 8549 |
. . . . 5
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ (𝐹 ∪ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∪ 𝐺) finSupp 𝑍 ↔ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin)) |
58 | 48, 53, 56, 57 | syl3anc 1496 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → ((𝐹 ∪ 𝐺) finSupp 𝑍 ↔ ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin)) |
59 | 46, 58 | mpbird 249 |
. . 3
⊢ ((𝜑 ∧ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)) → (𝐹 ∪ 𝐺) finSupp 𝑍) |
60 | 59 | ex 403 |
. 2
⊢ (𝜑 → ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → (𝐹 ∪ 𝐺) finSupp 𝑍)) |
61 | 42, 60 | impbid 204 |
1
⊢ (𝜑 → ((𝐹 ∪ 𝐺) finSupp 𝑍 ↔ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍))) |