Step | Hyp | Ref
| Expression |
1 | | r1rankidb 9801 |
. . . . . . 7
β’ (π΄ β βͺ (π
1 β On) β π΄ β
(π
1β(rankβπ΄))) |
2 | 1 | sspwd 4614 |
. . . . . 6
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β π«
(π
1β(rankβπ΄))) |
3 | | rankdmr1 9798 |
. . . . . . 7
β’
(rankβπ΄)
β dom π
1 |
4 | | r1sucg 9766 |
. . . . . . 7
β’
((rankβπ΄)
β dom π
1 β (π
1βsuc
(rankβπ΄)) = π«
(π
1β(rankβπ΄))) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
β’
(π
1βsuc (rankβπ΄)) = π«
(π
1β(rankβπ΄)) |
6 | 2, 5 | sseqtrrdi 4032 |
. . . . 5
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β
(π
1βsuc (rankβπ΄))) |
7 | | fvex 6903 |
. . . . . 6
β’
(π
1βsuc (rankβπ΄)) β V |
8 | 7 | elpw2 5344 |
. . . . 5
β’
(π« π΄ β
π« (π
1βsuc (rankβπ΄)) β π« π΄ β (π
1βsuc
(rankβπ΄))) |
9 | 6, 8 | sylibr 233 |
. . . 4
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β π«
(π
1βsuc (rankβπ΄))) |
10 | | r1funlim 9763 |
. . . . . . . 8
β’ (Fun
π
1 β§ Lim dom π
1) |
11 | 10 | simpri 484 |
. . . . . . 7
β’ Lim dom
π
1 |
12 | | limsuc 7840 |
. . . . . . 7
β’ (Lim dom
π
1 β ((rankβπ΄) β dom π
1 β
suc (rankβπ΄) β
dom π
1)) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
β’
((rankβπ΄)
β dom π
1 β suc (rankβπ΄) β dom
π
1) |
14 | 3, 13 | mpbi 229 |
. . . . 5
β’ suc
(rankβπ΄) β dom
π
1 |
15 | | r1sucg 9766 |
. . . . 5
β’ (suc
(rankβπ΄) β dom
π
1 β (π
1βsuc suc
(rankβπ΄)) = π«
(π
1βsuc (rankβπ΄))) |
16 | 14, 15 | ax-mp 5 |
. . . 4
β’
(π
1βsuc suc (rankβπ΄)) = π«
(π
1βsuc (rankβπ΄)) |
17 | 9, 16 | eleqtrrdi 2842 |
. . 3
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β
(π
1βsuc suc (rankβπ΄))) |
18 | | r1elwf 9793 |
. . 3
β’
(π« π΄ β
(π
1βsuc suc (rankβπ΄)) β π« π΄ β βͺ
(π
1 β On)) |
19 | 17, 18 | syl 17 |
. 2
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β βͺ (π
1 β On)) |
20 | | r1elssi 9802 |
. . 3
β’
(π« π΄ β
βͺ (π
1 β On) β
π« π΄ β βͺ (π
1 β On)) |
21 | | pwexr 7754 |
. . . 4
β’
(π« π΄ β
βͺ (π
1 β On) β π΄ β V) |
22 | | pwidg 4621 |
. . . 4
β’ (π΄ β V β π΄ β π« π΄) |
23 | 21, 22 | syl 17 |
. . 3
β’
(π« π΄ β
βͺ (π
1 β On) β π΄ β π« π΄) |
24 | 20, 23 | sseldd 3982 |
. 2
β’
(π« π΄ β
βͺ (π
1 β On) β π΄ β βͺ (π
1 β On)) |
25 | 19, 24 | impbii 208 |
1
β’ (π΄ β βͺ (π
1 β On) β π«
π΄ β βͺ (π
1 β On)) |