Step | Hyp | Ref
| Expression |
1 | | elfvdm 6928 |
. . 3
β’ (π΄ β
(π
1βπ΅) β π΅ β dom
π
1) |
2 | | r1val1 9783 |
. . . . . 6
β’ (π΅ β dom
π
1 β (π
1βπ΅) = βͺ
π₯ β π΅ π«
(π
1βπ₯)) |
3 | 2 | eleq2d 2819 |
. . . . 5
β’ (π΅ β dom
π
1 β (π΄ β (π
1βπ΅) β π΄ β βͺ
π₯ β π΅ π«
(π
1βπ₯))) |
4 | | eliun 5001 |
. . . . 5
β’ (π΄ β βͺ π₯ β π΅ π«
(π
1βπ₯) β βπ₯ β π΅ π΄ β π«
(π
1βπ₯)) |
5 | 3, 4 | bitrdi 286 |
. . . 4
β’ (π΅ β dom
π
1 β (π΄ β (π
1βπ΅) β βπ₯ β π΅ π΄ β π«
(π
1βπ₯))) |
6 | | r1funlim 9763 |
. . . . . . . . . . 11
β’ (Fun
π
1 β§ Lim dom π
1) |
7 | 6 | simpri 486 |
. . . . . . . . . 10
β’ Lim dom
π
1 |
8 | | limord 6424 |
. . . . . . . . . 10
β’ (Lim dom
π
1 β Ord dom π
1) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . 9
β’ Ord dom
π
1 |
10 | | ordtr1 6407 |
. . . . . . . . 9
β’ (Ord dom
π
1 β ((π₯ β π΅ β§ π΅ β dom π
1) β
π₯ β dom
π
1)) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . 8
β’ ((π₯ β π΅ β§ π΅ β dom π
1) β
π₯ β dom
π
1) |
12 | 11 | ancoms 459 |
. . . . . . 7
β’ ((π΅ β dom
π
1 β§ π₯ β π΅) β π₯ β dom
π
1) |
13 | | r1sucg 9766 |
. . . . . . . 8
β’ (π₯ β dom
π
1 β (π
1βsuc π₯) = π«
(π
1βπ₯)) |
14 | 13 | eleq2d 2819 |
. . . . . . 7
β’ (π₯ β dom
π
1 β (π΄ β (π
1βsuc
π₯) β π΄ β π«
(π
1βπ₯))) |
15 | 12, 14 | syl 17 |
. . . . . 6
β’ ((π΅ β dom
π
1 β§ π₯ β π΅) β (π΄ β (π
1βsuc
π₯) β π΄ β π«
(π
1βπ₯))) |
16 | | ordsson 7772 |
. . . . . . . . . 10
β’ (Ord dom
π
1 β dom π
1 β
On) |
17 | 9, 16 | ax-mp 5 |
. . . . . . . . 9
β’ dom
π
1 β On |
18 | 17, 12 | sselid 3980 |
. . . . . . . 8
β’ ((π΅ β dom
π
1 β§ π₯ β π΅) β π₯ β On) |
19 | | rabid 3452 |
. . . . . . . . 9
β’ (π₯ β {π₯ β On β£ π΄ β (π
1βsuc
π₯)} β (π₯ β On β§ π΄ β
(π
1βsuc π₯))) |
20 | | intss1 4967 |
. . . . . . . . 9
β’ (π₯ β {π₯ β On β£ π΄ β (π
1βsuc
π₯)} β β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)} β π₯) |
21 | 19, 20 | sylbir 234 |
. . . . . . . 8
β’ ((π₯ β On β§ π΄ β
(π
1βsuc π₯)) β β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)} β π₯) |
22 | 18, 21 | sylan 580 |
. . . . . . 7
β’ (((π΅ β dom
π
1 β§ π₯ β π΅) β§ π΄ β (π
1βsuc
π₯)) β β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)} β π₯) |
23 | 22 | ex 413 |
. . . . . 6
β’ ((π΅ β dom
π
1 β§ π₯ β π΅) β (π΄ β (π
1βsuc
π₯) β β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)} β π₯)) |
24 | 15, 23 | sylbird 259 |
. . . . 5
β’ ((π΅ β dom
π
1 β§ π₯ β π΅) β (π΄ β π«
(π
1βπ₯) β β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)} β π₯)) |
25 | 24 | reximdva 3168 |
. . . 4
β’ (π΅ β dom
π
1 β (βπ₯ β π΅ π΄ β π«
(π
1βπ₯) β βπ₯ β π΅ β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)} β π₯)) |
26 | 5, 25 | sylbid 239 |
. . 3
β’ (π΅ β dom
π
1 β (π΄ β (π
1βπ΅) β βπ₯ β π΅ β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)} β π₯)) |
27 | 1, 26 | mpcom 38 |
. 2
β’ (π΄ β
(π
1βπ΅) β βπ₯ β π΅ β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)} β π₯) |
28 | | r1elwf 9793 |
. . . . . . 7
β’ (π΄ β
(π
1βπ΅) β π΄ β βͺ
(π
1 β On)) |
29 | | rankvalb 9794 |
. . . . . . 7
β’ (π΄ β βͺ (π
1 β On) β
(rankβπ΄) = β© {π₯
β On β£ π΄ β
(π
1βsuc π₯)}) |
30 | 28, 29 | syl 17 |
. . . . . 6
β’ (π΄ β
(π
1βπ΅) β (rankβπ΄) = β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)}) |
31 | 30 | sseq1d 4013 |
. . . . 5
β’ (π΄ β
(π
1βπ΅) β ((rankβπ΄) β π₯ β β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)} β π₯)) |
32 | 31 | adantr 481 |
. . . 4
β’ ((π΄ β
(π
1βπ΅) β§ π₯ β π΅) β ((rankβπ΄) β π₯ β β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)} β π₯)) |
33 | | rankon 9792 |
. . . . . . 7
β’
(rankβπ΄)
β On |
34 | 17, 1 | sselid 3980 |
. . . . . . 7
β’ (π΄ β
(π
1βπ΅) β π΅ β On) |
35 | | ontr2 6411 |
. . . . . . 7
β’
(((rankβπ΄)
β On β§ π΅ β
On) β (((rankβπ΄)
β π₯ β§ π₯ β π΅) β (rankβπ΄) β π΅)) |
36 | 33, 34, 35 | sylancr 587 |
. . . . . 6
β’ (π΄ β
(π
1βπ΅) β (((rankβπ΄) β π₯ β§ π₯ β π΅) β (rankβπ΄) β π΅)) |
37 | 36 | expcomd 417 |
. . . . 5
β’ (π΄ β
(π
1βπ΅) β (π₯ β π΅ β ((rankβπ΄) β π₯ β (rankβπ΄) β π΅))) |
38 | 37 | imp 407 |
. . . 4
β’ ((π΄ β
(π
1βπ΅) β§ π₯ β π΅) β ((rankβπ΄) β π₯ β (rankβπ΄) β π΅)) |
39 | 32, 38 | sylbird 259 |
. . 3
β’ ((π΄ β
(π
1βπ΅) β§ π₯ β π΅) β (β©
{π₯ β On β£ π΄ β
(π
1βsuc π₯)} β π₯ β (rankβπ΄) β π΅)) |
40 | 39 | rexlimdva 3155 |
. 2
β’ (π΄ β
(π
1βπ΅) β (βπ₯ β π΅ β© {π₯ β On β£ π΄ β
(π
1βsuc π₯)} β π₯ β (rankβπ΄) β π΅)) |
41 | 27, 40 | mpd 15 |
1
β’ (π΄ β
(π
1βπ΅) β (rankβπ΄) β π΅) |