Step | Hyp | Ref
| Expression |
1 | | 0ex 5306 |
. . . 4
β’ β
β V |
2 | | eleq1 2819 |
. . . 4
β’ (π΄ = β
β (π΄ β V β β
β
V)) |
3 | 1, 2 | mpbiri 257 |
. . 3
β’ (π΄ = β
β π΄ β V) |
4 | | rabexg 5330 |
. . 3
β’ (π΄ β V β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
5 | 3, 4 | syl 17 |
. 2
β’ (π΄ = β
β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
6 | | neq0 4344 |
. . 3
β’ (Β¬
π΄ = β
β
βπ¦ π¦ β π΄) |
7 | | nfra1 3279 |
. . . . . 6
β’
β²π¦βπ¦ β π΄ (rankβπ₯) β (rankβπ¦) |
8 | | nfcv 2901 |
. . . . . 6
β’
β²π¦π΄ |
9 | 7, 8 | nfrabw 3466 |
. . . . 5
β’
β²π¦{π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} |
10 | 9 | nfel1 2917 |
. . . 4
β’
β²π¦{π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V |
11 | | rsp 3242 |
. . . . . . . 8
β’
(βπ¦ β
π΄ (rankβπ₯) β (rankβπ¦) β (π¦ β π΄ β (rankβπ₯) β (rankβπ¦))) |
12 | 11 | com12 32 |
. . . . . . 7
β’ (π¦ β π΄ β (βπ¦ β π΄ (rankβπ₯) β (rankβπ¦) β (rankβπ₯) β (rankβπ¦))) |
13 | 12 | adantr 479 |
. . . . . 6
β’ ((π¦ β π΄ β§ π₯ β π΄) β (βπ¦ β π΄ (rankβπ₯) β (rankβπ¦) β (rankβπ₯) β (rankβπ¦))) |
14 | 13 | ss2rabdv 4072 |
. . . . 5
β’ (π¦ β π΄ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)}) |
15 | | rankon 9792 |
. . . . . . . 8
β’
(rankβπ¦)
β On |
16 | | fveq2 6890 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (rankβπ₯) = (rankβπ€)) |
17 | 16 | sseq1d 4012 |
. . . . . . . . . . 11
β’ (π₯ = π€ β ((rankβπ₯) β (rankβπ¦) β (rankβπ€) β (rankβπ¦))) |
18 | 17 | elrab 3682 |
. . . . . . . . . 10
β’ (π€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β (π€ β π΄ β§ (rankβπ€) β (rankβπ¦))) |
19 | 18 | simprbi 495 |
. . . . . . . . 9
β’ (π€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β (rankβπ€) β (rankβπ¦)) |
20 | 19 | rgen 3061 |
. . . . . . . 8
β’
βπ€ β
{π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β (rankβπ¦) |
21 | | sseq2 4007 |
. . . . . . . . . 10
β’ (π§ = (rankβπ¦) β ((rankβπ€) β π§ β (rankβπ€) β (rankβπ¦))) |
22 | 21 | ralbidv 3175 |
. . . . . . . . 9
β’ (π§ = (rankβπ¦) β (βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β π§ β βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β (rankβπ¦))) |
23 | 22 | rspcev 3611 |
. . . . . . . 8
β’
(((rankβπ¦)
β On β§ βπ€
β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β (rankβπ¦)) β βπ§ β On βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β π§) |
24 | 15, 20, 23 | mp2an 688 |
. . . . . . 7
β’
βπ§ β On
βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β π§ |
25 | | bndrank 9838 |
. . . . . . 7
β’
(βπ§ β On
βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β π§ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β V) |
26 | 24, 25 | ax-mp 5 |
. . . . . 6
β’ {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β V |
27 | 26 | ssex 5320 |
. . . . 5
β’ ({π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
28 | 14, 27 | syl 17 |
. . . 4
β’ (π¦ β π΄ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
29 | 10, 28 | exlimi 2208 |
. . 3
β’
(βπ¦ π¦ β π΄ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
30 | 6, 29 | sylbi 216 |
. 2
β’ (Β¬
π΄ = β
β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
31 | 5, 30 | pm2.61i 182 |
1
β’ {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V |