Proof of Theorem ackbij1lem9
Step | Hyp | Ref
| Expression |
1 | | inss2 3796 |
. . . . . . . . . 10
⊢
(𝒫 ω ∩ Fin) ⊆ Fin |
2 | 1 | sseli 3564 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → 𝐴 ∈
Fin) |
3 | 2 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ∈ Fin) |
4 | | snfi 7923 |
. . . . . . . . . 10
⊢ {𝑦} ∈ Fin |
5 | | inss1 3795 |
. . . . . . . . . . . . . . . 16
⊢
(𝒫 ω ∩ Fin) ⊆ 𝒫 ω |
6 | 5 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → 𝐴 ∈
𝒫 ω) |
7 | 6 | elpwid 4118 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → 𝐴 ⊆
ω) |
8 | 7 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ⊆ ω) |
9 | | onfin2 8037 |
. . . . . . . . . . . . . 14
⊢ ω =
(On ∩ Fin) |
10 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (On ∩
Fin) ⊆ Fin |
11 | 9, 10 | eqsstri 3598 |
. . . . . . . . . . . . 13
⊢ ω
⊆ Fin |
12 | 8, 11 | syl6ss 3580 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ⊆ Fin) |
13 | 12 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ Fin) |
14 | | pwfi 8144 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ Fin ↔ 𝒫
𝑦 ∈
Fin) |
15 | 13, 14 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐴) → 𝒫 𝑦 ∈ Fin) |
16 | | xpfi 8116 |
. . . . . . . . . 10
⊢ (({𝑦} ∈ Fin ∧ 𝒫
𝑦 ∈ Fin) →
({𝑦} × 𝒫
𝑦) ∈
Fin) |
17 | 4, 15, 16 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐴) → ({𝑦} × 𝒫 𝑦) ∈ Fin) |
18 | 17 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∀𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
19 | | iunfi 8137 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ ∀𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) → ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
20 | 3, 18, 19 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
21 | | ficardid 8671 |
. . . . . . 7
⊢ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) |
23 | 1 | sseli 3564 |
. . . . . . . . 9
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → 𝐵 ∈
Fin) |
24 | 23 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ∈ Fin) |
25 | 5 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → 𝐵 ∈
𝒫 ω) |
26 | 25 | elpwid 4118 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → 𝐵 ⊆
ω) |
27 | 26 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ⊆ ω) |
28 | 27, 11 | syl6ss 3580 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ⊆ Fin) |
29 | 28 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ Fin) |
30 | 29, 14 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐵) → 𝒫 𝑦 ∈ Fin) |
31 | 4, 30, 16 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐵) → ({𝑦} × 𝒫 𝑦) ∈ Fin) |
32 | 31 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∀𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
33 | | iunfi 8137 |
. . . . . . . 8
⊢ ((𝐵 ∈ Fin ∧ ∀𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) → ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
34 | 24, 32, 33 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
35 | | ficardid 8671 |
. . . . . . 7
⊢ (∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) |
36 | 34, 35 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) |
37 | | cdaen 8878 |
. . . . . 6
⊢
(((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∧ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
38 | 22, 36, 37 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
39 | | djudisj 5480 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) = ∅) |
40 | 39 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) = ∅) |
41 | | cdaun 8877 |
. . . . . . 7
⊢
((∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin ∧ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin ∧ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∪ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
42 | 20, 34, 40, 41 | syl3anc 1318 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∪ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
43 | | iunxun 4541 |
. . . . . 6
⊢ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦) = (∪
𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∪ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) |
44 | 42, 43 | syl6breqr 4625 |
. . . . 5
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) |
45 | | entr 7894 |
. . . . 5
⊢
((((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∧ (∪
𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) |
46 | 38, 44, 45 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) |
47 | | carden2b 8676 |
. . . 4
⊢
(((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦) → (card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
48 | 46, 47 | syl 17 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) →
(card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
49 | | ficardom 8670 |
. . . . 5
⊢ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
50 | 20, 49 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
51 | | ficardom 8670 |
. . . . 5
⊢ (∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
52 | 34, 51 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
53 | | nnacda 8906 |
. . . 4
⊢
(((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ∈ ω ∧ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∈ ω) →
(card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
54 | 50, 52, 53 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) →
(card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
55 | 48, 54 | eqtr3d 2646 |
. 2
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
56 | | ackbij1lem6 8930 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩
Fin)) |
57 | 56 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩
Fin)) |
58 | | ackbij.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
59 | 58 | ackbij1lem7 8931 |
. . 3
⊢ ((𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin)
→ (𝐹‘(𝐴 ∪ 𝐵)) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
60 | 57, 59 | syl 17 |
. 2
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
61 | 58 | ackbij1lem7 8931 |
. . . 4
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦))) |
62 | 58 | ackbij1lem7 8931 |
. . . 4
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → (𝐹‘𝐵) = (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
63 | 61, 62 | oveqan12d 6568 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) +𝑜 (𝐹‘𝐵)) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
64 | 63 | 3adant3 1074 |
. 2
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹‘𝐴) +𝑜 (𝐹‘𝐵)) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
65 | 55, 60, 64 | 3eqtr4d 2654 |
1
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +𝑜 (𝐹‘𝐵))) |