Step | Hyp | Ref
| Expression |
1 | | cflem 10187 |
. . 3
β’ (π΄ β On β βπ₯βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
2 | | intexab 5297 |
. . 3
β’
(βπ₯βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β β© {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β V) |
3 | 1, 2 | sylib 217 |
. 2
β’ (π΄ β On β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β V) |
4 | | sseq2 3971 |
. . . . . . . 8
β’ (π£ = π΄ β (π¦ β π£ β π¦ β π΄)) |
5 | | raleq 3308 |
. . . . . . . 8
β’ (π£ = π΄ β (βπ§ β π£ βπ€ β π¦ π§ β π€ β βπ§ β π΄ βπ€ β π¦ π§ β π€)) |
6 | 4, 5 | anbi12d 632 |
. . . . . . 7
β’ (π£ = π΄ β ((π¦ β π£ β§ βπ§ β π£ βπ€ β π¦ π§ β π€) β (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
7 | 6 | anbi2d 630 |
. . . . . 6
β’ (π£ = π΄ β ((π₯ = (cardβπ¦) β§ (π¦ β π£ β§ βπ§ β π£ βπ€ β π¦ π§ β π€)) β (π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
8 | 7 | exbidv 1925 |
. . . . 5
β’ (π£ = π΄ β (βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π£ β§ βπ§ β π£ βπ€ β π¦ π§ β π€)) β βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)))) |
9 | 8 | abbidv 2802 |
. . . 4
β’ (π£ = π΄ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π£ β§ βπ§ β π£ βπ€ β π¦ π§ β π€))} = {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
10 | 9 | inteqd 4913 |
. . 3
β’ (π£ = π΄ β β© {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π£ β§ βπ§ β π£ βπ€ β π¦ π§ β π€))} = β© {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
11 | | df-cf 9882 |
. . 3
β’ cf =
(π£ β On β¦ β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π£ β§ βπ§ β π£ βπ€ β π¦ π§ β π€))}) |
12 | 10, 11 | fvmptg 6947 |
. 2
β’ ((π΄ β On β§ β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))} β V) β (cfβπ΄) = β©
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |
13 | 3, 12 | mpdan 686 |
1
β’ (π΄ β On β
(cfβπ΄) = β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))}) |