Step | Hyp | Ref
| Expression |
1 | | 0ex 5268 |
. . . 4
β’ β
β V |
2 | | eleq1 2822 |
. . . 4
β’ (π΄ = β
β (π΄ β V β β
β
V)) |
3 | 1, 2 | mpbiri 258 |
. . 3
β’ (π΄ = β
β π΄ β V) |
4 | | rabexg 5292 |
. . 3
β’ (π΄ β V β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
5 | 3, 4 | syl 17 |
. 2
β’ (π΄ = β
β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
6 | | neq0 4309 |
. . 3
β’ (Β¬
π΄ = β
β
βπ¦ π¦ β π΄) |
7 | | nfra1 3266 |
. . . . . 6
β’
β²π¦βπ¦ β π΄ (rankβπ₯) β (rankβπ¦) |
8 | | nfcv 2904 |
. . . . . 6
β’
β²π¦π΄ |
9 | 7, 8 | nfrabw 3442 |
. . . . 5
β’
β²π¦{π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} |
10 | 9 | nfel1 2920 |
. . . 4
β’
β²π¦{π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V |
11 | | rsp 3229 |
. . . . . . . 8
β’
(βπ¦ β
π΄ (rankβπ₯) β (rankβπ¦) β (π¦ β π΄ β (rankβπ₯) β (rankβπ¦))) |
12 | 11 | com12 32 |
. . . . . . 7
β’ (π¦ β π΄ β (βπ¦ β π΄ (rankβπ₯) β (rankβπ¦) β (rankβπ₯) β (rankβπ¦))) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π¦ β π΄ β§ π₯ β π΄) β (βπ¦ β π΄ (rankβπ₯) β (rankβπ¦) β (rankβπ₯) β (rankβπ¦))) |
14 | 13 | ss2rabdv 4037 |
. . . . 5
β’ (π¦ β π΄ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)}) |
15 | | rankon 9739 |
. . . . . . . 8
β’
(rankβπ¦)
β On |
16 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (rankβπ₯) = (rankβπ€)) |
17 | 16 | sseq1d 3979 |
. . . . . . . . . . 11
β’ (π₯ = π€ β ((rankβπ₯) β (rankβπ¦) β (rankβπ€) β (rankβπ¦))) |
18 | 17 | elrab 3649 |
. . . . . . . . . 10
β’ (π€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β (π€ β π΄ β§ (rankβπ€) β (rankβπ¦))) |
19 | 18 | simprbi 498 |
. . . . . . . . 9
β’ (π€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β (rankβπ€) β (rankβπ¦)) |
20 | 19 | rgen 3063 |
. . . . . . . 8
β’
βπ€ β
{π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β (rankβπ¦) |
21 | | sseq2 3974 |
. . . . . . . . . 10
β’ (π§ = (rankβπ¦) β ((rankβπ€) β π§ β (rankβπ€) β (rankβπ¦))) |
22 | 21 | ralbidv 3171 |
. . . . . . . . 9
β’ (π§ = (rankβπ¦) β (βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β π§ β βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β (rankβπ¦))) |
23 | 22 | rspcev 3583 |
. . . . . . . 8
β’
(((rankβπ¦)
β On β§ βπ€
β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β (rankβπ¦)) β βπ§ β On βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β π§) |
24 | 15, 20, 23 | mp2an 691 |
. . . . . . 7
β’
βπ§ β On
βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β π§ |
25 | | bndrank 9785 |
. . . . . . 7
β’
(βπ§ β On
βπ€ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} (rankβπ€) β π§ β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β V) |
26 | 24, 25 | ax-mp 5 |
. . . . . 6
β’ {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β V |
27 | 26 | ssex 5282 |
. . . . 5
β’ ({π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β {π₯ β π΄ β£ (rankβπ₯) β (rankβπ¦)} β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
28 | 14, 27 | syl 17 |
. . . 4
β’ (π¦ β π΄ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
29 | 10, 28 | exlimi 2211 |
. . 3
β’
(βπ¦ π¦ β π΄ β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
30 | 6, 29 | sylbi 216 |
. 2
β’ (Β¬
π΄ = β
β {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V) |
31 | 5, 30 | pm2.61i 182 |
1
β’ {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} β V |