| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ackbij.f |
⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 2 |
|
elinel2 |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ Fin ) |
| 3 |
2
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ∈ Fin ) |
| 4 |
|
snfi |
⊢ { 𝑦 } ∈ Fin |
| 5 |
|
elinel1 |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ 𝒫 ω ) |
| 6 |
5
|
elpwid |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ⊆ ω ) |
| 7 |
6
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ⊆ ω ) |
| 8 |
|
onfin2 |
⊢ ω = ( On ∩ Fin ) |
| 9 |
|
inss2 |
⊢ ( On ∩ Fin ) ⊆ Fin |
| 10 |
8 9
|
eqsstri |
⊢ ω ⊆ Fin |
| 11 |
7 10
|
sstrdi |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ⊆ Fin ) |
| 12 |
11
|
sselda |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ Fin ) |
| 13 |
|
pwfi |
⊢ ( 𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin ) |
| 14 |
12 13
|
sylib |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐴 ) → 𝒫 𝑦 ∈ Fin ) |
| 15 |
|
xpfi |
⊢ ( ( { 𝑦 } ∈ Fin ∧ 𝒫 𝑦 ∈ Fin ) → ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) |
| 16 |
4 14 15
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐴 ) → ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) |
| 17 |
16
|
ralrimiva |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∀ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) |
| 18 |
|
iunfi |
⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) → ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) |
| 19 |
3 17 18
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) |
| 20 |
|
ficardid |
⊢ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin → ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) |
| 21 |
19 20
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) |
| 22 |
|
elinel2 |
⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → 𝐵 ∈ Fin ) |
| 23 |
22
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ∈ Fin ) |
| 24 |
|
elinel1 |
⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → 𝐵 ∈ 𝒫 ω ) |
| 25 |
24
|
elpwid |
⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → 𝐵 ⊆ ω ) |
| 26 |
25
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ⊆ ω ) |
| 27 |
26 10
|
sstrdi |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ⊆ Fin ) |
| 28 |
27
|
sselda |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ Fin ) |
| 29 |
28 13
|
sylib |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝒫 𝑦 ∈ Fin ) |
| 30 |
4 29 15
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) |
| 31 |
30
|
ralrimiva |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∀ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) |
| 32 |
|
iunfi |
⊢ ( ( 𝐵 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) → ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) |
| 33 |
23 31 32
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) |
| 34 |
|
ficardid |
⊢ ( ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin → ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) |
| 35 |
33 34
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) |
| 36 |
|
djuen |
⊢ ( ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∧ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) → ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 37 |
21 35 36
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 38 |
|
djudisj |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) = ∅ ) |
| 39 |
38
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) = ∅ ) |
| 40 |
|
endjudisj |
⊢ ( ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ∧ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ∧ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) = ∅ ) → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∪ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 41 |
19 33 39 40
|
syl3anc |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∪ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 42 |
|
iunxun |
⊢ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) = ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∪ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) |
| 43 |
41 42
|
breqtrrdi |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) |
| 44 |
|
entr |
⊢ ( ( ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ∧ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) → ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) |
| 45 |
37 43 44
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) |
| 46 |
|
carden2b |
⊢ ( ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) → ( card ‘ ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) = ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 47 |
45 46
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) = ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 48 |
|
ficardom |
⊢ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin → ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω ) |
| 49 |
19 48
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω ) |
| 50 |
|
ficardom |
⊢ ( ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin → ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω ) |
| 51 |
33 50
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω ) |
| 52 |
|
nnadju |
⊢ ( ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω ∧ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω ) → ( card ‘ ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) |
| 53 |
49 51 52
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) |
| 54 |
47 53
|
eqtr3d |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) |
| 55 |
|
ackbij1lem6 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝒫 ω ∩ Fin ) ) |
| 56 |
55
|
3adant3 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝒫 ω ∩ Fin ) ) |
| 57 |
1
|
ackbij1lem7 |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 58 |
56 57
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 59 |
1
|
ackbij1lem7 |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ 𝐴 ) = ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 60 |
1
|
ackbij1lem7 |
⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ 𝐵 ) = ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
| 61 |
59 60
|
oveqan12d |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ 𝐵 ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) |
| 62 |
61
|
3adant3 |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ 𝐵 ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) |
| 63 |
54 58 62
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ 𝐵 ) ) ) |