Step | Hyp | Ref
| Expression |
1 | | nfcv 2904 |
. . . 4
β’
β²π§{π₯ β£ π} |
2 | | nfab1 2906 |
. . . 4
β’
β²π₯{π₯ β£ π} |
3 | | nfv 1918 |
. . . . 5
β’
β²π₯(rankβπ§) β (rankβπ¦) |
4 | 2, 3 | nfralw 3309 |
. . . 4
β’
β²π₯βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦) |
5 | | nfv 1918 |
. . . 4
β’
β²π§βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦) |
6 | | fveq2 6892 |
. . . . . 6
β’ (π§ = π₯ β (rankβπ§) = (rankβπ₯)) |
7 | 6 | sseq1d 4014 |
. . . . 5
β’ (π§ = π₯ β ((rankβπ§) β (rankβπ¦) β (rankβπ₯) β (rankβπ¦))) |
8 | 7 | ralbidv 3178 |
. . . 4
β’ (π§ = π₯ β (βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦) β βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦))) |
9 | 1, 2, 4, 5, 8 | cbvrabw 3468 |
. . 3
β’ {π§ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦)} = {π₯ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦)} |
10 | | df-rab 3434 |
. . 3
β’ {π₯ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦)} = {π₯ β£ (π₯ β {π₯ β£ π} β§ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦))} |
11 | | abid 2714 |
. . . . 5
β’ (π₯ β {π₯ β£ π} β π) |
12 | | df-ral 3063 |
. . . . . 6
β’
(βπ¦ β
{π₯ β£ π} (rankβπ₯) β (rankβπ¦) β βπ¦(π¦ β {π₯ β£ π} β (rankβπ₯) β (rankβπ¦))) |
13 | | df-sbc 3779 |
. . . . . . . 8
β’
([π¦ / π₯]π β π¦ β {π₯ β£ π}) |
14 | 13 | imbi1i 350 |
. . . . . . 7
β’
(([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)) β (π¦ β {π₯ β£ π} β (rankβπ₯) β (rankβπ¦))) |
15 | 14 | albii 1822 |
. . . . . 6
β’
(βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)) β βπ¦(π¦ β {π₯ β£ π} β (rankβπ₯) β (rankβπ¦))) |
16 | 12, 15 | bitr4i 278 |
. . . . 5
β’
(βπ¦ β
{π₯ β£ π} (rankβπ₯) β (rankβπ¦) β βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦))) |
17 | 11, 16 | anbi12i 628 |
. . . 4
β’ ((π₯ β {π₯ β£ π} β§ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦)) β (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))) |
18 | 17 | abbii 2803 |
. . 3
β’ {π₯ β£ (π₯ β {π₯ β£ π} β§ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦))} = {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} |
19 | 9, 10, 18 | 3eqtri 2765 |
. 2
β’ {π§ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦)} = {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} |
20 | | scottex 9880 |
. 2
β’ {π§ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦)} β V |
21 | 19, 20 | eqeltrri 2831 |
1
β’ {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} β V |