| Step | Hyp | Ref
| Expression |
|---|
| 1 | | sneq 4638 |
. . . 4
β’ (π = π΄ β {π} = {π΄}) |
| 2 | 1 | fveq2d 6895 |
. . 3
β’ (π = π΄ β (πΉβ{π}) = (πΉβ{π΄})) |
| 3 | | pweq 4616 |
. . . 4
β’ (π = π΄ β π« π = π« π΄) |
| 4 | 3 | fveq2d 6895 |
. . 3
β’ (π = π΄ β (cardβπ« π) = (cardβπ« π΄)) |
| 5 | 2, 4 | eqeq12d 2748 |
. 2
β’ (π = π΄ β ((πΉβ{π}) = (cardβπ« π) β (πΉβ{π΄}) = (cardβπ« π΄))) |
| 6 | | ackbij1lem4 10217 |
. . . 4
β’ (π β Ο β {π} β (π« Ο
β© Fin)) |
| 7 | | ackbij.f |
. . . . 5
β’ πΉ = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
| 8 | 7 | ackbij1lem7 10220 |
. . . 4
β’ ({π} β (π« Ο
β© Fin) β (πΉβ{π}) = (cardββͺ π¦ β {π} ({π¦} Γ π« π¦))) |
| 9 | 6, 8 | syl 17 |
. . 3
β’ (π β Ο β (πΉβ{π}) = (cardββͺ π¦ β {π} ({π¦} Γ π« π¦))) |
| 10 | | vex 3478 |
. . . . . 6
β’ π β V |
| 11 | | sneq 4638 |
. . . . . . 7
β’ (π¦ = π β {π¦} = {π}) |
| 12 | | pweq 4616 |
. . . . . . 7
β’ (π¦ = π β π« π¦ = π« π) |
| 13 | 11, 12 | xpeq12d 5707 |
. . . . . 6
β’ (π¦ = π β ({π¦} Γ π« π¦) = ({π} Γ π« π)) |
| 14 | 10, 13 | iunxsn 5094 |
. . . . 5
β’ βͺ π¦ β {π} ({π¦} Γ π« π¦) = ({π} Γ π« π) |
| 15 | 14 | fveq2i 6894 |
. . . 4
β’
(cardββͺ π¦ β {π} ({π¦} Γ π« π¦)) = (cardβ({π} Γ π« π)) |
| 16 | | vpwex 5375 |
. . . . . 6
β’ π«
π β V |
| 17 | | xpsnen2g 9064 |
. . . . . 6
β’ ((π β V β§ π« π β V) β ({π} Γ π« π) β π« π) |
| 18 | 10, 16, 17 | mp2an 690 |
. . . . 5
β’ ({π} Γ π« π) β π« π |
| 19 | | carden2b 9961 |
. . . . 5
β’ (({π} Γ π« π) β π« π β (cardβ({π} Γ π« π)) = (cardβπ« π)) |
| 20 | 18, 19 | ax-mp 5 |
. . . 4
β’
(cardβ({π}
Γ π« π)) =
(cardβπ« π) |
| 21 | 15, 20 | eqtri 2760 |
. . 3
β’
(cardββͺ π¦ β {π} ({π¦} Γ π« π¦)) = (cardβπ« π) |
| 22 | 9, 21 | eqtrdi 2788 |
. 2
β’ (π β Ο β (πΉβ{π}) = (cardβπ« π)) |
| 23 | 5, 22 | vtoclga 3565 |
1
β’ (π΄ β Ο β (πΉβ{π΄}) = (cardβπ« π΄)) |
