Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . 3
β’ (π¦ = πΆ β (rankβπ¦) = (rankβπΆ)) |
2 | 1 | sseq2d 3980 |
. 2
β’ (π¦ = πΆ β ((rankβπ΅) β (rankβπ¦) β (rankβπ΅) β (rankβπΆ))) |
3 | | scottelrankd.1 |
. . . . 5
β’ (π β π΅ β Scott π΄) |
4 | | df-scott 42608 |
. . . . 5
β’ Scott
π΄ = {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} |
5 | 3, 4 | eleqtrdi 2844 |
. . . 4
β’ (π β π΅ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)}) |
6 | | fveq2 6846 |
. . . . . . 7
β’ (π₯ = π΅ β (rankβπ₯) = (rankβπ΅)) |
7 | 6 | sseq1d 3979 |
. . . . . 6
β’ (π₯ = π΅ β ((rankβπ₯) β (rankβπ¦) β (rankβπ΅) β (rankβπ¦))) |
8 | 7 | ralbidv 3171 |
. . . . 5
β’ (π₯ = π΅ β (βπ¦ β π΄ (rankβπ₯) β (rankβπ¦) β βπ¦ β π΄ (rankβπ΅) β (rankβπ¦))) |
9 | 8 | elrab 3649 |
. . . 4
β’ (π΅ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β (π΅ β π΄ β§ βπ¦ β π΄ (rankβπ΅) β (rankβπ¦))) |
10 | 5, 9 | sylib 217 |
. . 3
β’ (π β (π΅ β π΄ β§ βπ¦ β π΄ (rankβπ΅) β (rankβπ¦))) |
11 | 10 | simprd 497 |
. 2
β’ (π β βπ¦ β π΄ (rankβπ΅) β (rankβπ¦)) |
12 | | scottelrankd.2 |
. . . 4
β’ (π β πΆ β Scott π΄) |
13 | 12, 4 | eleqtrdi 2844 |
. . 3
β’ (π β πΆ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)}) |
14 | | elrabi 3643 |
. . 3
β’ (πΆ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β πΆ β π΄) |
15 | 13, 14 | syl 17 |
. 2
β’ (π β πΆ β π΄) |
16 | 2, 11, 15 | rspcdva 3584 |
1
β’ (π β (rankβπ΅) β (rankβπΆ)) |