Proof of Theorem ackbij1lem9
Step | Hyp | Ref
| Expression |
1 | | inss2 3969 |
. . . . . . . . . 10
⊢
(𝒫 ω ∩ Fin) ⊆ Fin |
2 | 1 | sseli 3732 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → 𝐴 ∈
Fin) |
3 | 2 | 3ad2ant1 1127 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ∈ Fin) |
4 | | snfi 8195 |
. . . . . . . . . 10
⊢ {𝑦} ∈ Fin |
5 | | inss1 3968 |
. . . . . . . . . . . . . . . 16
⊢
(𝒫 ω ∩ Fin) ⊆ 𝒫 ω |
6 | 5 | sseli 3732 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → 𝐴 ∈
𝒫 ω) |
7 | 6 | elpwid 4306 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → 𝐴 ⊆
ω) |
8 | 7 | 3ad2ant1 1127 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ⊆ ω) |
9 | | onfin2 8309 |
. . . . . . . . . . . . . 14
⊢ ω =
(On ∩ Fin) |
10 | | inss2 3969 |
. . . . . . . . . . . . . 14
⊢ (On ∩
Fin) ⊆ Fin |
11 | 9, 10 | eqsstri 3768 |
. . . . . . . . . . . . 13
⊢ ω
⊆ Fin |
12 | 8, 11 | syl6ss 3748 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ⊆ Fin) |
13 | 12 | sselda 3736 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ Fin) |
14 | | pwfi 8418 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ Fin ↔ 𝒫
𝑦 ∈
Fin) |
15 | 13, 14 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐴) → 𝒫 𝑦 ∈ Fin) |
16 | | xpfi 8388 |
. . . . . . . . . 10
⊢ (({𝑦} ∈ Fin ∧ 𝒫
𝑦 ∈ Fin) →
({𝑦} × 𝒫
𝑦) ∈
Fin) |
17 | 4, 15, 16 | sylancr 698 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐴) → ({𝑦} × 𝒫 𝑦) ∈ Fin) |
18 | 17 | ralrimiva 3096 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∀𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
19 | | iunfi 8411 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ ∀𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) → ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
20 | 3, 18, 19 | syl2anc 696 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
21 | | ficardid 8970 |
. . . . . . 7
⊢ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) |
23 | 1 | sseli 3732 |
. . . . . . . . 9
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → 𝐵 ∈
Fin) |
24 | 23 | 3ad2ant2 1128 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ∈ Fin) |
25 | 5 | sseli 3732 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → 𝐵 ∈
𝒫 ω) |
26 | 25 | elpwid 4306 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → 𝐵 ⊆
ω) |
27 | 26 | 3ad2ant2 1128 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ⊆ ω) |
28 | 27, 11 | syl6ss 3748 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ⊆ Fin) |
29 | 28 | sselda 3736 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ Fin) |
30 | 29, 14 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐵) → 𝒫 𝑦 ∈ Fin) |
31 | 4, 30, 16 | sylancr 698 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ 𝐵) → ({𝑦} × 𝒫 𝑦) ∈ Fin) |
32 | 31 | ralrimiva 3096 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∀𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
33 | | iunfi 8411 |
. . . . . . . 8
⊢ ((𝐵 ∈ Fin ∧ ∀𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) → ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
34 | 24, 32, 33 | syl2anc 696 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin) |
35 | | ficardid 8970 |
. . . . . . 7
⊢ (∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) |
36 | 34, 35 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) |
37 | | cdaen 9179 |
. . . . . 6
⊢
(((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∧ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
38 | 22, 36, 37 | syl2anc 696 |
. . . . 5
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
39 | | djudisj 5711 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) = ∅) |
40 | 39 | 3ad2ant3 1129 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) = ∅) |
41 | | cdaun 9178 |
. . . . . . 7
⊢
((∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin ∧ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin ∧ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∪ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
42 | 20, 34, 40, 41 | syl3anc 1473 |
. . . . . 6
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∪ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
43 | | iunxun 4749 |
. . . . . 6
⊢ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦) = (∪
𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∪ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) |
44 | 42, 43 | syl6breqr 4838 |
. . . . 5
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) |
45 | | entr 8165 |
. . . . 5
⊢
((((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∧ (∪
𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) +𝑐 ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) |
46 | 38, 44, 45 | syl2anc 696 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) |
47 | | carden2b 8975 |
. . . 4
⊢
(((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) ≈ ∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦) → (card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
48 | 46, 47 | syl 17 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) →
(card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
49 | | ficardom 8969 |
. . . . 5
⊢ (∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
50 | 20, 49 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
51 | | ficardom 8969 |
. . . . 5
⊢ (∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦) ∈ Fin → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
52 | 34, 51 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∈ ω) |
53 | | nnacda 9207 |
. . . 4
⊢
(((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) ∈ ω ∧ (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)) ∈ ω) →
(card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
54 | 50, 52, 53 | syl2anc 696 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) →
(card‘((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑐 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
55 | 48, 54 | eqtr3d 2788 |
. 2
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦)) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
56 | | ackbij1lem6 9231 |
. . . 4
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩
Fin)) |
57 | 56 | 3adant3 1126 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩
Fin)) |
58 | | ackbij.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) |
59 | 58 | ackbij1lem7 9232 |
. . 3
⊢ ((𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin)
→ (𝐹‘(𝐴 ∪ 𝐵)) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
60 | 57, 59 | syl 17 |
. 2
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = (card‘∪ 𝑦 ∈ (𝐴 ∪ 𝐵)({𝑦} × 𝒫 𝑦))) |
61 | 58 | ackbij1lem7 9232 |
. . . 4
⊢ (𝐴 ∈ (𝒫 ω ∩
Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦))) |
62 | 58 | ackbij1lem7 9232 |
. . . 4
⊢ (𝐵 ∈ (𝒫 ω ∩
Fin) → (𝐹‘𝐵) = (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦))) |
63 | 61, 62 | oveqan12d 6824 |
. . 3
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) +𝑜 (𝐹‘𝐵)) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
64 | 63 | 3adant3 1126 |
. 2
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹‘𝐴) +𝑜 (𝐹‘𝐵)) = ((card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)) +𝑜 (card‘∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝒫 𝑦)))) |
65 | 55, 60, 64 | 3eqtr4d 2796 |
1
⊢ ((𝐴 ∈ (𝒫 ω ∩
Fin) ∧ 𝐵 ∈
(𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +𝑜 (𝐹‘𝐵))) |