Step | Hyp | Ref
| Expression |
1 | | elhf 34812 |
. 2
β’ (π΄ β Hf β βπ₯ β Ο π΄ β
(π
1βπ₯)) |
2 | | omon 7818 |
. . 3
β’ (Ο
β On β¨ Ο = On) |
3 | | nnon 7812 |
. . . . . . . . 9
β’ (π₯ β Ο β π₯ β On) |
4 | | elhf2.1 |
. . . . . . . . . 10
β’ π΄ β V |
5 | 4 | rankr1a 9780 |
. . . . . . . . 9
β’ (π₯ β On β (π΄ β
(π
1βπ₯) β (rankβπ΄) β π₯)) |
6 | 3, 5 | syl 17 |
. . . . . . . 8
β’ (π₯ β Ο β (π΄ β
(π
1βπ₯) β (rankβπ΄) β π₯)) |
7 | 6 | adantl 483 |
. . . . . . 7
β’ ((Ο
β On β§ π₯ β
Ο) β (π΄ β
(π
1βπ₯) β (rankβπ΄) β π₯)) |
8 | | elnn 7817 |
. . . . . . . . 9
β’
(((rankβπ΄)
β π₯ β§ π₯ β Ο) β
(rankβπ΄) β
Ο) |
9 | 8 | expcom 415 |
. . . . . . . 8
β’ (π₯ β Ο β
((rankβπ΄) β
π₯ β (rankβπ΄) β
Ο)) |
10 | 9 | adantl 483 |
. . . . . . 7
β’ ((Ο
β On β§ π₯ β
Ο) β ((rankβπ΄) β π₯ β (rankβπ΄) β Ο)) |
11 | 7, 10 | sylbid 239 |
. . . . . 6
β’ ((Ο
β On β§ π₯ β
Ο) β (π΄ β
(π
1βπ₯) β (rankβπ΄) β Ο)) |
12 | 11 | rexlimdva 3149 |
. . . . 5
β’ (Ο
β On β (βπ₯
β Ο π΄ β
(π
1βπ₯) β (rankβπ΄) β Ο)) |
13 | | peano2 7831 |
. . . . . . . 8
β’
((rankβπ΄)
β Ο β suc (rankβπ΄) β Ο) |
14 | 13 | adantr 482 |
. . . . . . 7
β’
(((rankβπ΄)
β Ο β§ Ο β On) β suc (rankβπ΄) β
Ο) |
15 | | r1rankid 9803 |
. . . . . . . . . 10
β’ (π΄ β V β π΄ β
(π
1β(rankβπ΄))) |
16 | 4, 15 | mp1i 13 |
. . . . . . . . 9
β’
(((rankβπ΄)
β Ο β§ Ο β On) β π΄ β
(π
1β(rankβπ΄))) |
17 | 4 | elpw 4568 |
. . . . . . . . 9
β’ (π΄ β π«
(π
1β(rankβπ΄)) β π΄ β
(π
1β(rankβπ΄))) |
18 | 16, 17 | sylibr 233 |
. . . . . . . 8
β’
(((rankβπ΄)
β Ο β§ Ο β On) β π΄ β π«
(π
1β(rankβπ΄))) |
19 | | nnon 7812 |
. . . . . . . . . 10
β’
((rankβπ΄)
β Ο β (rankβπ΄) β On) |
20 | | r1suc 9714 |
. . . . . . . . . 10
β’
((rankβπ΄)
β On β (π
1βsuc (rankβπ΄)) = π«
(π
1β(rankβπ΄))) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
β’
((rankβπ΄)
β Ο β (π
1βsuc (rankβπ΄)) = π«
(π
1β(rankβπ΄))) |
22 | 21 | adantr 482 |
. . . . . . . 8
β’
(((rankβπ΄)
β Ο β§ Ο β On) β (π
1βsuc
(rankβπ΄)) = π«
(π
1β(rankβπ΄))) |
23 | 18, 22 | eleqtrrd 2837 |
. . . . . . 7
β’
(((rankβπ΄)
β Ο β§ Ο β On) β π΄ β (π
1βsuc
(rankβπ΄))) |
24 | | fveq2 6846 |
. . . . . . . . 9
β’ (π₯ = suc (rankβπ΄) β
(π
1βπ₯) = (π
1βsuc
(rankβπ΄))) |
25 | 24 | eleq2d 2820 |
. . . . . . . 8
β’ (π₯ = suc (rankβπ΄) β (π΄ β (π
1βπ₯) β π΄ β (π
1βsuc
(rankβπ΄)))) |
26 | 25 | rspcev 3583 |
. . . . . . 7
β’ ((suc
(rankβπ΄) β
Ο β§ π΄ β
(π
1βsuc (rankβπ΄))) β βπ₯ β Ο π΄ β (π
1βπ₯)) |
27 | 14, 23, 26 | syl2anc 585 |
. . . . . 6
β’
(((rankβπ΄)
β Ο β§ Ο β On) β βπ₯ β Ο π΄ β (π
1βπ₯)) |
28 | 27 | expcom 415 |
. . . . 5
β’ (Ο
β On β ((rankβπ΄) β Ο β βπ₯ β Ο π΄ β
(π
1βπ₯))) |
29 | 12, 28 | impbid 211 |
. . . 4
β’ (Ο
β On β (βπ₯
β Ο π΄ β
(π
1βπ₯) β (rankβπ΄) β Ο)) |
30 | 4 | tz9.13 9735 |
. . . . . 6
β’
βπ₯ β On
π΄ β
(π
1βπ₯) |
31 | | rankon 9739 |
. . . . . 6
β’
(rankβπ΄)
β On |
32 | 30, 31 | 2th 264 |
. . . . 5
β’
(βπ₯ β On
π΄ β
(π
1βπ₯) β (rankβπ΄) β On) |
33 | | rexeq 3309 |
. . . . . 6
β’ (Ο
= On β (βπ₯
β Ο π΄ β
(π
1βπ₯) β βπ₯ β On π΄ β (π
1βπ₯))) |
34 | | eleq2 2823 |
. . . . . 6
β’ (Ο
= On β ((rankβπ΄)
β Ο β (rankβπ΄) β On)) |
35 | 33, 34 | bibi12d 346 |
. . . . 5
β’ (Ο
= On β ((βπ₯
β Ο π΄ β
(π
1βπ₯) β (rankβπ΄) β Ο) β (βπ₯ β On π΄ β (π
1βπ₯) β (rankβπ΄) β On))) |
36 | 32, 35 | mpbiri 258 |
. . . 4
β’ (Ο
= On β (βπ₯
β Ο π΄ β
(π
1βπ₯) β (rankβπ΄) β Ο)) |
37 | 29, 36 | jaoi 856 |
. . 3
β’ ((Ο
β On β¨ Ο = On) β (βπ₯ β Ο π΄ β (π
1βπ₯) β (rankβπ΄) β
Ο)) |
38 | 2, 37 | ax-mp 5 |
. 2
β’
(βπ₯ β
Ο π΄ β
(π
1βπ₯) β (rankβπ΄) β Ο) |
39 | 1, 38 | bitri 275 |
1
β’ (π΄ β Hf β
(rankβπ΄) β
Ο) |