Step | Hyp | Ref
| Expression |
1 | | sneq 4600 |
. . . 4
β’ (π = π΄ β {π} = {π΄}) |
2 | 1 | fveq2d 6850 |
. . 3
β’ (π = π΄ β (πΉβ{π}) = (πΉβ{π΄})) |
3 | | pweq 4578 |
. . . 4
β’ (π = π΄ β π« π = π« π΄) |
4 | 3 | fveq2d 6850 |
. . 3
β’ (π = π΄ β (cardβπ« π) = (cardβπ« π΄)) |
5 | 2, 4 | eqeq12d 2749 |
. 2
β’ (π = π΄ β ((πΉβ{π}) = (cardβπ« π) β (πΉβ{π΄}) = (cardβπ« π΄))) |
6 | | ackbij1lem4 10167 |
. . . 4
β’ (π β Ο β {π} β (π« Ο
β© Fin)) |
7 | | ackbij.f |
. . . . 5
β’ πΉ = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
8 | 7 | ackbij1lem7 10170 |
. . . 4
β’ ({π} β (π« Ο
β© Fin) β (πΉβ{π}) = (cardββͺ π¦ β {π} ({π¦} Γ π« π¦))) |
9 | 6, 8 | syl 17 |
. . 3
β’ (π β Ο β (πΉβ{π}) = (cardββͺ π¦ β {π} ({π¦} Γ π« π¦))) |
10 | | vex 3451 |
. . . . . 6
β’ π β V |
11 | | sneq 4600 |
. . . . . . 7
β’ (π¦ = π β {π¦} = {π}) |
12 | | pweq 4578 |
. . . . . . 7
β’ (π¦ = π β π« π¦ = π« π) |
13 | 11, 12 | xpeq12d 5668 |
. . . . . 6
β’ (π¦ = π β ({π¦} Γ π« π¦) = ({π} Γ π« π)) |
14 | 10, 13 | iunxsn 5055 |
. . . . 5
β’ βͺ π¦ β {π} ({π¦} Γ π« π¦) = ({π} Γ π« π) |
15 | 14 | fveq2i 6849 |
. . . 4
β’
(cardββͺ π¦ β {π} ({π¦} Γ π« π¦)) = (cardβ({π} Γ π« π)) |
16 | | vpwex 5336 |
. . . . . 6
β’ π«
π β V |
17 | | xpsnen2g 9015 |
. . . . . 6
β’ ((π β V β§ π« π β V) β ({π} Γ π« π) β π« π) |
18 | 10, 16, 17 | mp2an 691 |
. . . . 5
β’ ({π} Γ π« π) β π« π |
19 | | carden2b 9911 |
. . . . 5
β’ (({π} Γ π« π) β π« π β (cardβ({π} Γ π« π)) = (cardβπ« π)) |
20 | 18, 19 | ax-mp 5 |
. . . 4
β’
(cardβ({π}
Γ π« π)) =
(cardβπ« π) |
21 | 15, 20 | eqtri 2761 |
. . 3
β’
(cardββͺ π¦ β {π} ({π¦} Γ π« π¦)) = (cardβπ« π) |
22 | 9, 21 | eqtrdi 2789 |
. 2
β’ (π β Ο β (πΉβ{π}) = (cardβπ« π)) |
23 | 5, 22 | vtoclga 3536 |
1
β’ (π΄ β Ο β (πΉβ{π΄}) = (cardβπ« π΄)) |