Proof of Theorem ackbij1lem9
Step | Hyp | Ref
| Expression |
1 | | elinel2 4110 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → 𝐴 ∈
Fin) |
2 | 1 | 3ad2ant1 1135 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ∈ Fin) |
3 | | snfi 8721 |
. . . . . . . . . 10
⊢ {𝑦} ∈ Fin |
4 | | elinel1 4109 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → 𝐴 ∈
𝒫 ω) |
5 | 4 | elpwid 4524 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → 𝐴 ⊆
ω) |
6 | 5 | 3ad2ant1 1135 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ⊆ ω) |
7 | | onfin2 8871 |
. . . . . . . . . . . . . 14
⊢ ω =
(On ∩ Fin) |
8 | | inss2 4144 |
. . . . . . . . . . . . . 14
⊢ (On ∩
Fin) ⊆ Fin |
9 | 7, 8 | eqsstri 3935 |
. . . . . . . . . . . . 13
⊢ ω
⊆ Fin |
10 | 6, 9 | sstrdi 3913 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ⊆ Fin) |
11 | 10 | sselda 3901 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ Fin) |
12 | | pwfi 8856 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ Fin ↔ 𝒫
𝑦 ∈
Fin) |
13 | 11, 12 | sylib 221 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐴) → 𝒫 𝑦 ∈ Fin) |
14 | | xpfi 8942 |
. . . . . . . . . 10
⊢ (({𝑦} ∈ Fin ∧ 𝒫
𝑦 ∈ Fin) →
({𝑦} × 𝒫
𝑦) ∈
Fin) |
15 | 3, 13, 14 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐴) → ({𝑦} × 𝒫 𝑦) ∈ Fin) |
16 | 15 | ralrimiva 3105 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∀𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
17 | | iunfi 8964 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ ∀𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) → ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
18 | 2, 16, 17 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
19 | | ficardid 9578 |
. . . . . . 7
⊢ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) |
20 | 18, 19 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) |
21 | | elinel2 4110 |
. . . . . . . . 9
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → 𝐵 ∈
Fin) |
22 | 21 | 3ad2ant2 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ∈ Fin) |
23 | | elinel1 4109 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → 𝐵 ∈
𝒫 ω) |
24 | 23 | elpwid 4524 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → 𝐵 ⊆
ω) |
25 | 24 | 3ad2ant2 1136 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ⊆ ω) |
26 | 25, 9 | sstrdi 3913 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ⊆ Fin) |
27 | 26 | sselda 3901 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ Fin) |
28 | 27, 12 | sylib 221 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐵) → 𝒫 𝑦 ∈ Fin) |
29 | 3, 28, 14 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐵) → ({𝑦} × 𝒫 𝑦) ∈ Fin) |
30 | 29 | ralrimiva 3105 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∀𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
31 | | iunfi 8964 |
. . . . . . . 8
⊢ ((𝐵 ∈ Fin ∧ ∀𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) → ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
32 | 22, 30, 31 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
33 | | ficardid 9578 |
. . . . . . 7
⊢ (∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) |
34 | 32, 33 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) |
35 | | djuen 9783 |
. . . . . 6
⊢
(((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∧ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ⊔ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
36 | 20, 34, 35 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ⊔ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
37 | | djudisj 6030 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) = ∅) |
38 | 37 | 3ad2ant3 1137 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) = ∅) |
39 | | endjudisj 9782 |
. . . . . . 7
⊢
((∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin ∧ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin ∧ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ⊔ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∪ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
40 | 18, 32, 38, 39 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ⊔ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∪ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
41 | | iunxun 5002 |
. . . . . 6
⊢ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦) = (∪
𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∪ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) |
42 | 40, 41 | breqtrrdi 5095 |
. . . . 5
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ⊔ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) |
43 | | entr 8680 |
. . . . 5
⊢
((((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ⊔ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∧ (∪
𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ⊔ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) |
44 | 36, 42, 43 | syl2anc 587 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) |
45 | | carden2b 9583 |
. . . 4
⊢
(((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦) → (card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
46 | 44, 45 | syl 17 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) →
(card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
47 | | ficardom 9577 |
. . . . 5
⊢ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
48 | 18, 47 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
49 | | ficardom 9577 |
. . . . 5
⊢ (∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
50 | 32, 49 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
51 | | nnadju 9811 |
. . . 4
⊢
(((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ∈ ω ∧ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∈ ω) →
(card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +o (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
52 | 48, 50, 51 | syl2anc 587 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) →
(card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ⊔ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +o (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
53 | 46, 52 | eqtr3d 2779 |
. 2
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +o (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
54 | | ackbij1lem6 9839 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩
Fin)) |
55 | 54 | 3adant3 1134 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩
Fin)) |
56 | | ackbij.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
57 | 56 | ackbij1lem7 9840 |
. . 3
⊢ ((𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin)
→ (𝐹‘(𝐴 ∪ 𝐵)) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
58 | 55, 57 | syl 17 |
. 2
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
59 | 56 | ackbij1lem7 9840 |
. . . 4
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦))) |
60 | 56 | ackbij1lem7 9840 |
. . . 4
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → (𝐹‘𝐵) = (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
61 | 59, 60 | oveqan12d 7232 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) +o (𝐹‘𝐵)) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +o (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
62 | 61 | 3adant3 1134 |
. 2
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹‘𝐴) +o (𝐹‘𝐵)) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +o (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
63 | 53, 58, 62 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +o (𝐹‘𝐵))) |