Step | Hyp | Ref
| Expression |
1 | | rankidn 9817 |
. . . 4
β’ (π΄ β βͺ (π
1 β On) β Β¬ π΄ β
(π
1β(rankβπ΄))) |
2 | | rankon 9790 |
. . . . . . 7
β’
(rankβπ΄)
β On |
3 | | r1suc 9765 |
. . . . . . 7
β’
((rankβπ΄)
β On β (π
1βsuc (rankβπ΄)) = π«
(π
1β(rankβπ΄))) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
β’
(π
1βsuc (rankβπ΄)) = π«
(π
1β(rankβπ΄)) |
5 | 4 | eleq2i 2826 |
. . . . 5
β’
(π« π΄ β
(π
1βsuc (rankβπ΄)) β π« π΄ β π«
(π
1β(rankβπ΄))) |
6 | | elpwi 4610 |
. . . . . 6
β’
(π« π΄ β
π« (π
1β(rankβπ΄)) β π« π΄ β
(π
1β(rankβπ΄))) |
7 | | pwidg 4623 |
. . . . . 6
β’ (π΄ β βͺ (π
1 β On) β π΄ β π« π΄) |
8 | | ssel 3976 |
. . . . . 6
β’
(π« π΄ β
(π
1β(rankβπ΄)) β (π΄ β π« π΄ β π΄ β
(π
1β(rankβπ΄)))) |
9 | 6, 7, 8 | syl2imc 41 |
. . . . 5
β’ (π΄ β βͺ (π
1 β On) β (π«
π΄ β π«
(π
1β(rankβπ΄)) β π΄ β
(π
1β(rankβπ΄)))) |
10 | 5, 9 | biimtrid 241 |
. . . 4
β’ (π΄ β βͺ (π
1 β On) β (π«
π΄ β
(π
1βsuc (rankβπ΄)) β π΄ β
(π
1β(rankβπ΄)))) |
11 | 1, 10 | mtod 197 |
. . 3
β’ (π΄ β βͺ (π
1 β On) β Β¬
π« π΄ β
(π
1βsuc (rankβπ΄))) |
12 | | r1rankidb 9799 |
. . . . . . 7
β’ (π΄ β βͺ (π
1 β On) β π΄ β
(π
1β(rankβπ΄))) |
13 | 12 | sspwd 4616 |
. . . . . 6
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β π«
(π
1β(rankβπ΄))) |
14 | 13, 4 | sseqtrrdi 4034 |
. . . . 5
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β
(π
1βsuc (rankβπ΄))) |
15 | | fvex 6905 |
. . . . . 6
β’
(π
1βsuc (rankβπ΄)) β V |
16 | 15 | elpw2 5346 |
. . . . 5
β’
(π« π΄ β
π« (π
1βsuc (rankβπ΄)) β π« π΄ β (π
1βsuc
(rankβπ΄))) |
17 | 14, 16 | sylibr 233 |
. . . 4
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β π«
(π
1βsuc (rankβπ΄))) |
18 | 2 | onsuci 7827 |
. . . . 5
β’ suc
(rankβπ΄) β
On |
19 | | r1suc 9765 |
. . . . 5
β’ (suc
(rankβπ΄) β On
β (π
1βsuc suc (rankβπ΄)) = π«
(π
1βsuc (rankβπ΄))) |
20 | 18, 19 | ax-mp 5 |
. . . 4
β’
(π
1βsuc suc (rankβπ΄)) = π«
(π
1βsuc (rankβπ΄)) |
21 | 17, 20 | eleqtrrdi 2845 |
. . 3
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β
(π
1βsuc suc (rankβπ΄))) |
22 | | pwwf 9802 |
. . . 4
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β βͺ (π
1 β On)) |
23 | | rankr1c 9816 |
. . . 4
β’
(π« π΄ β
βͺ (π
1 β On) β (suc
(rankβπ΄) =
(rankβπ« π΄)
β (Β¬ π« π΄
β (π
1βsuc (rankβπ΄)) β§ π« π΄ β (π
1βsuc suc
(rankβπ΄))))) |
24 | 22, 23 | sylbi 216 |
. . 3
β’ (π΄ β βͺ (π
1 β On) β (suc
(rankβπ΄) =
(rankβπ« π΄)
β (Β¬ π« π΄
β (π
1βsuc (rankβπ΄)) β§ π« π΄ β (π
1βsuc suc
(rankβπ΄))))) |
25 | 11, 21, 24 | mpbir2and 712 |
. 2
β’ (π΄ β βͺ (π
1 β On) β suc
(rankβπ΄) =
(rankβπ« π΄)) |
26 | 25 | eqcomd 2739 |
1
β’ (π΄ β βͺ (π
1 β On) β
(rankβπ« π΄) =
suc (rankβπ΄)) |