Step | Hyp | Ref
| Expression |
1 | | df-scott 42608 |
. 2
β’ Scott
{π₯ β£ π} = {π§ β {π₯ β£ π} β£ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€)} |
2 | | df-rab 3407 |
. 2
β’ {π§ β {π₯ β£ π} β£ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€)} = {π§ β£ (π§ β {π₯ β£ π} β§ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€))} |
3 | | eqabc 2876 |
. . 3
β’ ({π§ β£ (π§ β {π₯ β£ π} β§ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€))} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} β βπ§((π§ β {π₯ β£ π} β§ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€)) β π§ β {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))})) |
4 | | nfsab1 2718 |
. . . . . 6
β’
β²π₯ π§ β {π₯ β£ π} |
5 | | nfab1 2906 |
. . . . . . 7
β’
β²π₯{π₯ β£ π} |
6 | | nfv 1918 |
. . . . . . 7
β’
β²π₯(rankβπ§) β (rankβπ€) |
7 | 5, 6 | nfralw 3293 |
. . . . . 6
β’
β²π₯βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€) |
8 | 4, 7 | nfan 1903 |
. . . . 5
β’
β²π₯(π§ β {π₯ β£ π} β§ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€)) |
9 | | vex 3451 |
. . . . 5
β’ π§ β V |
10 | | abid 2714 |
. . . . . . 7
β’ (π₯ β {π₯ β£ π} β π) |
11 | | eleq1w 2817 |
. . . . . . 7
β’ (π₯ = π§ β (π₯ β {π₯ β£ π} β π§ β {π₯ β£ π})) |
12 | 10, 11 | bitr3id 285 |
. . . . . 6
β’ (π₯ = π§ β (π β π§ β {π₯ β£ π})) |
13 | | df-clab 2711 |
. . . . . . . . . . . 12
β’ (π¦ β {π₯ β£ π} β [π¦ / π₯]π) |
14 | | scottabf.1 |
. . . . . . . . . . . . 13
β’
β²π₯π |
15 | | scottabf.2 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (π β π)) |
16 | 14, 15 | sbiev 2309 |
. . . . . . . . . . . 12
β’ ([π¦ / π₯]π β π) |
17 | 13, 16 | bitr2i 276 |
. . . . . . . . . . 11
β’ (π β π¦ β {π₯ β£ π}) |
18 | | eleq1w 2817 |
. . . . . . . . . . 11
β’ (π¦ = π€ β (π¦ β {π₯ β£ π} β π€ β {π₯ β£ π})) |
19 | 17, 18 | bitrid 283 |
. . . . . . . . . 10
β’ (π¦ = π€ β (π β π€ β {π₯ β£ π})) |
20 | 19 | adantl 483 |
. . . . . . . . 9
β’ ((π₯ = π§ β§ π¦ = π€) β (π β π€ β {π₯ β£ π})) |
21 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π₯ = π§ β§ π¦ = π€) β π₯ = π§) |
22 | 21 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π₯ = π§ β§ π¦ = π€) β (rankβπ₯) = (rankβπ§)) |
23 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π₯ = π§ β§ π¦ = π€) β π¦ = π€) |
24 | 23 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π₯ = π§ β§ π¦ = π€) β (rankβπ¦) = (rankβπ€)) |
25 | 22, 24 | sseq12d 3981 |
. . . . . . . . 9
β’ ((π₯ = π§ β§ π¦ = π€) β ((rankβπ₯) β (rankβπ¦) β (rankβπ§) β (rankβπ€))) |
26 | 20, 25 | imbi12d 345 |
. . . . . . . 8
β’ ((π₯ = π§ β§ π¦ = π€) β ((π β (rankβπ₯) β (rankβπ¦)) β (π€ β {π₯ β£ π} β (rankβπ§) β (rankβπ€)))) |
27 | 26 | cbvaldvaw 2042 |
. . . . . . 7
β’ (π₯ = π§ β (βπ¦(π β (rankβπ₯) β (rankβπ¦)) β βπ€(π€ β {π₯ β£ π} β (rankβπ§) β (rankβπ€)))) |
28 | | df-ral 3062 |
. . . . . . 7
β’
(βπ€ β
{π₯ β£ π} (rankβπ§) β (rankβπ€) β βπ€(π€ β {π₯ β£ π} β (rankβπ§) β (rankβπ€))) |
29 | 27, 28 | bitr4di 289 |
. . . . . 6
β’ (π₯ = π§ β (βπ¦(π β (rankβπ₯) β (rankβπ¦)) β βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€))) |
30 | 12, 29 | anbi12d 632 |
. . . . 5
β’ (π₯ = π§ β ((π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦))) β (π§ β {π₯ β£ π} β§ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€)))) |
31 | 8, 9, 30 | elabf 3631 |
. . . 4
β’ (π§ β {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} β (π§ β {π₯ β£ π} β§ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€))) |
32 | 31 | bicomi 223 |
. . 3
β’ ((π§ β {π₯ β£ π} β§ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€)) β π§ β {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))}) |
33 | 3, 32 | mpgbir 1802 |
. 2
β’ {π§ β£ (π§ β {π₯ β£ π} β§ βπ€ β {π₯ β£ π} (rankβπ§) β (rankβπ€))} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} |
34 | 1, 2, 33 | 3eqtri 2765 |
1
β’ Scott
{π₯ β£ π} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} |