Step | Hyp | Ref
| Expression |
1 | | nfcv 2903 |
. . . 4
β’
β²π§{π₯ β£ π} |
2 | | nfab1 2905 |
. . . 4
β’
β²π₯{π₯ β£ π} |
3 | | nfv 1917 |
. . . . 5
β’
β²π₯(rankβπ§) β (rankβπ¦) |
4 | 2, 3 | nfralw 3308 |
. . . 4
β’
β²π₯βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦) |
5 | | nfv 1917 |
. . . 4
β’
β²π§βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦) |
6 | | fveq2 6891 |
. . . . . 6
β’ (π§ = π₯ β (rankβπ§) = (rankβπ₯)) |
7 | 6 | sseq1d 4013 |
. . . . 5
β’ (π§ = π₯ β ((rankβπ§) β (rankβπ¦) β (rankβπ₯) β (rankβπ¦))) |
8 | 7 | ralbidv 3177 |
. . . 4
β’ (π§ = π₯ β (βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦) β βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦))) |
9 | 1, 2, 4, 5, 8 | cbvrabw 3467 |
. . 3
β’ {π§ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦)} = {π₯ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦)} |
10 | | df-rab 3433 |
. . 3
β’ {π₯ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦)} = {π₯ β£ (π₯ β {π₯ β£ π} β§ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦))} |
11 | | abid 2713 |
. . . . 5
β’ (π₯ β {π₯ β£ π} β π) |
12 | | df-ral 3062 |
. . . . . 6
β’
(βπ¦ β
{π₯ β£ π} (rankβπ₯) β (rankβπ¦) β βπ¦(π¦ β {π₯ β£ π} β (rankβπ₯) β (rankβπ¦))) |
13 | | df-sbc 3778 |
. . . . . . . 8
β’
([π¦ / π₯]π β π¦ β {π₯ β£ π}) |
14 | 13 | imbi1i 349 |
. . . . . . 7
β’
(([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)) β (π¦ β {π₯ β£ π} β (rankβπ₯) β (rankβπ¦))) |
15 | 14 | albii 1821 |
. . . . . 6
β’
(βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)) β βπ¦(π¦ β {π₯ β£ π} β (rankβπ₯) β (rankβπ¦))) |
16 | 12, 15 | bitr4i 277 |
. . . . 5
β’
(βπ¦ β
{π₯ β£ π} (rankβπ₯) β (rankβπ¦) β βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦))) |
17 | 11, 16 | anbi12i 627 |
. . . 4
β’ ((π₯ β {π₯ β£ π} β§ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦)) β (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))) |
18 | 17 | abbii 2802 |
. . 3
β’ {π₯ β£ (π₯ β {π₯ β£ π} β§ βπ¦ β {π₯ β£ π} (rankβπ₯) β (rankβπ¦))} = {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} |
19 | 9, 10, 18 | 3eqtri 2764 |
. 2
β’ {π§ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦)} = {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} |
20 | | scottex 9882 |
. 2
β’ {π§ β {π₯ β£ π} β£ βπ¦ β {π₯ β£ π} (rankβπ§) β (rankβπ¦)} β V |
21 | 19, 20 | eqeltrri 2830 |
1
β’ {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} β V |