Step | Hyp | Ref
| Expression |
1 | | elinel2 4160 |
. . . . . . . . 9
β’ (π΄ β (π« Ο β©
Fin) β π΄ β
Fin) |
2 | 1 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β π΄ β Fin) |
3 | | snfi 8994 |
. . . . . . . . . 10
β’ {π¦} β Fin |
4 | | elinel1 4159 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (π« Ο β©
Fin) β π΄ β
π« Ο) |
5 | 4 | elpwid 4573 |
. . . . . . . . . . . . . 14
β’ (π΄ β (π« Ο β©
Fin) β π΄ β
Ο) |
6 | 5 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β π΄ β Ο) |
7 | | onfin2 9181 |
. . . . . . . . . . . . . 14
β’ Ο =
(On β© Fin) |
8 | | inss2 4193 |
. . . . . . . . . . . . . 14
β’ (On β©
Fin) β Fin |
9 | 7, 8 | eqsstri 3982 |
. . . . . . . . . . . . 13
β’ Ο
β Fin |
10 | 6, 9 | sstrdi 3960 |
. . . . . . . . . . . 12
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β π΄ β Fin) |
11 | 10 | sselda 3948 |
. . . . . . . . . . 11
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β§ π¦ β π΄) β π¦ β Fin) |
12 | | pwfi 9128 |
. . . . . . . . . . 11
β’ (π¦ β Fin β π«
π¦ β
Fin) |
13 | 11, 12 | sylib 217 |
. . . . . . . . . 10
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β§ π¦ β π΄) β π« π¦ β Fin) |
14 | | xpfi 9267 |
. . . . . . . . . 10
β’ (({π¦} β Fin β§ π«
π¦ β Fin) β
({π¦} Γ π«
π¦) β
Fin) |
15 | 3, 13, 14 | sylancr 588 |
. . . . . . . . 9
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β§ π¦ β π΄) β ({π¦} Γ π« π¦) β Fin) |
16 | 15 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β βπ¦ β π΄ ({π¦} Γ π« π¦) β Fin) |
17 | | iunfi 9290 |
. . . . . . . 8
β’ ((π΄ β Fin β§ βπ¦ β π΄ ({π¦} Γ π« π¦) β Fin) β βͺ π¦ β π΄ ({π¦} Γ π« π¦) β Fin) |
18 | 2, 16, 17 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β βͺ π¦ β π΄ ({π¦} Γ π« π¦) β Fin) |
19 | | ficardid 9906 |
. . . . . . 7
β’ (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β Fin β (cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β βͺ π¦ β π΄ ({π¦} Γ π« π¦)) |
20 | 18, 19 | syl 17 |
. . . . . 6
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β βͺ π¦ β π΄ ({π¦} Γ π« π¦)) |
21 | | elinel2 4160 |
. . . . . . . . 9
β’ (π΅ β (π« Ο β©
Fin) β π΅ β
Fin) |
22 | 21 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β π΅ β Fin) |
23 | | elinel1 4159 |
. . . . . . . . . . . . . . 15
β’ (π΅ β (π« Ο β©
Fin) β π΅ β
π« Ο) |
24 | 23 | elpwid 4573 |
. . . . . . . . . . . . . 14
β’ (π΅ β (π« Ο β©
Fin) β π΅ β
Ο) |
25 | 24 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β π΅ β Ο) |
26 | 25, 9 | sstrdi 3960 |
. . . . . . . . . . . 12
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β π΅ β Fin) |
27 | 26 | sselda 3948 |
. . . . . . . . . . 11
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β§ π¦ β π΅) β π¦ β Fin) |
28 | 27, 12 | sylib 217 |
. . . . . . . . . 10
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β§ π¦ β π΅) β π« π¦ β Fin) |
29 | 3, 28, 14 | sylancr 588 |
. . . . . . . . 9
β’ (((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β§ π¦ β π΅) β ({π¦} Γ π« π¦) β Fin) |
30 | 29 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β βπ¦ β π΅ ({π¦} Γ π« π¦) β Fin) |
31 | | iunfi 9290 |
. . . . . . . 8
β’ ((π΅ β Fin β§ βπ¦ β π΅ ({π¦} Γ π« π¦) β Fin) β βͺ π¦ β π΅ ({π¦} Γ π« π¦) β Fin) |
32 | 22, 30, 31 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β βͺ π¦ β π΅ ({π¦} Γ π« π¦) β Fin) |
33 | | ficardid 9906 |
. . . . . . 7
β’ (βͺ π¦ β π΅ ({π¦} Γ π« π¦) β Fin β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)) β βͺ π¦ β π΅ ({π¦} Γ π« π¦)) |
34 | 32, 33 | syl 17 |
. . . . . 6
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)) β βͺ π¦ β π΅ ({π¦} Γ π« π¦)) |
35 | | djuen 10113 |
. . . . . 6
β’
(((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β βͺ π¦ β π΄ ({π¦} Γ π« π¦) β§ (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)) β βͺ π¦ β π΅ ({π¦} Γ π« π¦)) β ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦))) β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β βͺ π¦ β π΅ ({π¦} Γ π« π¦))) |
36 | 20, 34, 35 | syl2anc 585 |
. . . . 5
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦))) β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β βͺ π¦ β π΅ ({π¦} Γ π« π¦))) |
37 | | djudisj 6123 |
. . . . . . . 8
β’ ((π΄ β© π΅) = β
β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β© βͺ
π¦ β π΅ ({π¦} Γ π« π¦)) = β
) |
38 | 37 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β© βͺ
π¦ β π΅ ({π¦} Γ π« π¦)) = β
) |
39 | | endjudisj 10112 |
. . . . . . 7
β’
((βͺ π¦ β π΄ ({π¦} Γ π« π¦) β Fin β§ βͺ π¦ β π΅ ({π¦} Γ π« π¦) β Fin β§ (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β© βͺ
π¦ β π΅ ({π¦} Γ π« π¦)) = β
) β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β βͺ π¦ β π΅ ({π¦} Γ π« π¦)) β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) βͺ βͺ
π¦ β π΅ ({π¦} Γ π« π¦))) |
40 | 18, 32, 38, 39 | syl3anc 1372 |
. . . . . 6
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β βͺ π¦ β π΅ ({π¦} Γ π« π¦)) β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) βͺ βͺ
π¦ β π΅ ({π¦} Γ π« π¦))) |
41 | | iunxun 5058 |
. . . . . 6
β’ βͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦) = (βͺ
π¦ β π΄ ({π¦} Γ π« π¦) βͺ βͺ
π¦ β π΅ ({π¦} Γ π« π¦)) |
42 | 40, 41 | breqtrrdi 5151 |
. . . . 5
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β βͺ π¦ β π΅ ({π¦} Γ π« π¦)) β βͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦)) |
43 | | entr 8952 |
. . . . 5
β’
((((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦))) β (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β βͺ π¦ β π΅ ({π¦} Γ π« π¦)) β§ (βͺ
π¦ β π΄ ({π¦} Γ π« π¦) β βͺ π¦ β π΅ ({π¦} Γ π« π¦)) β βͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦)) β ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦))) β βͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦)) |
44 | 36, 42, 43 | syl2anc 585 |
. . . 4
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦))) β βͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦)) |
45 | | carden2b 9911 |
. . . 4
β’
(((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦))) β βͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦) β (cardβ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)))) = (cardββͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦))) |
46 | 44, 45 | syl 17 |
. . 3
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β
(cardβ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)))) = (cardββͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦))) |
47 | | ficardom 9905 |
. . . . 5
β’ (βͺ π¦ β π΄ ({π¦} Γ π« π¦) β Fin β (cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β Ο) |
48 | 18, 47 | syl 17 |
. . . 4
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β Ο) |
49 | | ficardom 9905 |
. . . . 5
β’ (βͺ π¦ β π΅ ({π¦} Γ π« π¦) β Fin β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)) β Ο) |
50 | 32, 49 | syl 17 |
. . . 4
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)) β Ο) |
51 | | nnadju 10141 |
. . . 4
β’
(((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β Ο β§ (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)) β Ο) β
(cardβ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)))) = ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) +o (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)))) |
52 | 48, 50, 51 | syl2anc 585 |
. . 3
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β
(cardβ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) β (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)))) = ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) +o (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)))) |
53 | 46, 52 | eqtr3d 2775 |
. 2
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (cardββͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦)) = ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) +o (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)))) |
54 | | ackbij1lem6 10169 |
. . . 4
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β (π΄ βͺ π΅) β (π« Ο β©
Fin)) |
55 | 54 | 3adant3 1133 |
. . 3
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (π΄ βͺ π΅) β (π« Ο β©
Fin)) |
56 | | ackbij.f |
. . . 4
β’ πΉ = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
57 | 56 | ackbij1lem7 10170 |
. . 3
β’ ((π΄ βͺ π΅) β (π« Ο β© Fin)
β (πΉβ(π΄ βͺ π΅)) = (cardββͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦))) |
58 | 55, 57 | syl 17 |
. 2
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (πΉβ(π΄ βͺ π΅)) = (cardββͺ π¦ β (π΄ βͺ π΅)({π¦} Γ π« π¦))) |
59 | 56 | ackbij1lem7 10170 |
. . . 4
β’ (π΄ β (π« Ο β©
Fin) β (πΉβπ΄) = (cardββͺ π¦ β π΄ ({π¦} Γ π« π¦))) |
60 | 56 | ackbij1lem7 10170 |
. . . 4
β’ (π΅ β (π« Ο β©
Fin) β (πΉβπ΅) = (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦))) |
61 | 59, 60 | oveqan12d 7380 |
. . 3
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin)) β ((πΉβπ΄) +o (πΉβπ΅)) = ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) +o (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)))) |
62 | 61 | 3adant3 1133 |
. 2
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β ((πΉβπ΄) +o (πΉβπ΅)) = ((cardββͺ π¦ β π΄ ({π¦} Γ π« π¦)) +o (cardββͺ π¦ β π΅ ({π¦} Γ π« π¦)))) |
63 | 53, 58, 62 | 3eqtr4d 2783 |
1
β’ ((π΄ β (π« Ο β©
Fin) β§ π΅ β
(π« Ο β© Fin) β§ (π΄ β© π΅) = β
) β (πΉβ(π΄ βͺ π΅)) = ((πΉβπ΄) +o (πΉβπ΅))) |