Step | Hyp | Ref
| Expression |
1 | | eleq1 2820 |
. . . . 5
β’ (π₯ = π΄ β (π₯ β (π
1βπ΅) β π΄ β (π
1βπ΅))) |
2 | | pweq 4616 |
. . . . . 6
β’ (π₯ = π΄ β π« π₯ = π« π΄) |
3 | 2 | eleq1d 2817 |
. . . . 5
β’ (π₯ = π΄ β (π« π₯ β (π
1βsuc
π΅) β π« π΄ β
(π
1βsuc π΅))) |
4 | 1, 3 | bibi12d 345 |
. . . 4
β’ (π₯ = π΄ β ((π₯ β (π
1βπ΅) β π« π₯ β
(π
1βsuc π΅)) β (π΄ β (π
1βπ΅) β π« π΄ β
(π
1βsuc π΅)))) |
5 | 4 | imbi2d 340 |
. . 3
β’ (π₯ = π΄ β ((π΅ β On β (π₯ β (π
1βπ΅) β π« π₯ β
(π
1βsuc π΅))) β (π΅ β On β (π΄ β (π
1βπ΅) β π« π΄ β
(π
1βsuc π΅))))) |
6 | | vex 3477 |
. . . . . . 7
β’ π₯ β V |
7 | 6 | rankr1a 9837 |
. . . . . 6
β’ (π΅ β On β (π₯ β
(π
1βπ΅) β (rankβπ₯) β π΅)) |
8 | | eloni 6374 |
. . . . . . 7
β’ (π΅ β On β Ord π΅) |
9 | | ordsucelsuc 7814 |
. . . . . . 7
β’ (Ord
π΅ β ((rankβπ₯) β π΅ β suc (rankβπ₯) β suc π΅)) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (π΅ β On β
((rankβπ₯) β
π΅ β suc
(rankβπ₯) β suc
π΅)) |
11 | 7, 10 | bitrd 279 |
. . . . 5
β’ (π΅ β On β (π₯ β
(π
1βπ΅) β suc (rankβπ₯) β suc π΅)) |
12 | 6 | rankpw 9844 |
. . . . . 6
β’
(rankβπ« π₯) = suc (rankβπ₯) |
13 | 12 | eleq1i 2823 |
. . . . 5
β’
((rankβπ« π₯) β suc π΅ β suc (rankβπ₯) β suc π΅) |
14 | 11, 13 | bitr4di 289 |
. . . 4
β’ (π΅ β On β (π₯ β
(π
1βπ΅) β (rankβπ« π₯) β suc π΅)) |
15 | | onsuc 7803 |
. . . . 5
β’ (π΅ β On β suc π΅ β On) |
16 | 6 | pwex 5378 |
. . . . . 6
β’ π«
π₯ β V |
17 | 16 | rankr1a 9837 |
. . . . 5
β’ (suc
π΅ β On β
(π« π₯ β
(π
1βsuc π΅) β (rankβπ« π₯) β suc π΅)) |
18 | 15, 17 | syl 17 |
. . . 4
β’ (π΅ β On β (π«
π₯ β
(π
1βsuc π΅) β (rankβπ« π₯) β suc π΅)) |
19 | 14, 18 | bitr4d 282 |
. . 3
β’ (π΅ β On β (π₯ β
(π
1βπ΅) β π« π₯ β (π
1βsuc
π΅))) |
20 | 5, 19 | vtoclg 3542 |
. 2
β’ (π΄ β V β (π΅ β On β (π΄ β
(π
1βπ΅) β π« π΄ β (π
1βsuc
π΅)))) |
21 | | elex 3492 |
. . . 4
β’ (π΄ β
(π
1βπ΅) β π΄ β V) |
22 | | elex 3492 |
. . . . 5
β’
(π« π΄ β
(π
1βsuc π΅) β π« π΄ β V) |
23 | | pwexb 7757 |
. . . . 5
β’ (π΄ β V β π« π΄ β V) |
24 | 22, 23 | sylibr 233 |
. . . 4
β’
(π« π΄ β
(π
1βsuc π΅) β π΄ β V) |
25 | 21, 24 | pm5.21ni 377 |
. . 3
β’ (Β¬
π΄ β V β (π΄ β
(π
1βπ΅) β π« π΄ β (π
1βsuc
π΅))) |
26 | 25 | a1d 25 |
. 2
β’ (Β¬
π΄ β V β (π΅ β On β (π΄ β
(π
1βπ΅) β π« π΄ β (π
1βsuc
π΅)))) |
27 | 20, 26 | pm2.61i 182 |
1
β’ (π΅ β On β (π΄ β
(π
1βπ΅) β π« π΄ β (π
1βsuc
π΅))) |