Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . . . . . 8
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( M βπ))) β π β π΄) |
2 | | limsuc 7789 |
. . . . . . . . 9
β’ (Lim
π΄ β (π β π΄ β suc π β π΄)) |
3 | 2 | ad2antrr 725 |
. . . . . . . 8
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( M βπ))) β (π β π΄ β suc π β π΄)) |
4 | 1, 3 | mpbid 231 |
. . . . . . 7
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( M βπ))) β suc π β π΄) |
5 | | simprr 772 |
. . . . . . . 8
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( M βπ))) β π₯ β ( M βπ)) |
6 | | limord 6381 |
. . . . . . . . . . . 12
β’ (Lim
π΄ β Ord π΄) |
7 | | elex 3465 |
. . . . . . . . . . . 12
β’ (π΄ β π β π΄ β V) |
8 | 6, 7 | anim12i 614 |
. . . . . . . . . . 11
β’ ((Lim
π΄ β§ π΄ β π) β (Ord π΄ β§ π΄ β V)) |
9 | | elon2 6332 |
. . . . . . . . . . 11
β’ (π΄ β On β (Ord π΄ β§ π΄ β V)) |
10 | 8, 9 | sylibr 233 |
. . . . . . . . . 10
β’ ((Lim
π΄ β§ π΄ β π) β π΄ β On) |
11 | | onelon 6346 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π β π΄) β π β On) |
12 | 10, 1, 11 | syl2an2r 684 |
. . . . . . . . 9
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( M βπ))) β π β On) |
13 | | madeoldsuc 27243 |
. . . . . . . . 9
β’ (π β On β ( M
βπ) = ( O βsuc
π)) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( M βπ))) β ( M βπ) = ( O βsuc π)) |
15 | 5, 14 | eleqtrd 2836 |
. . . . . . 7
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( M βπ))) β π₯ β ( O βsuc π)) |
16 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = suc π β ( O βπ) = ( O βsuc π)) |
17 | 16 | eleq2d 2820 |
. . . . . . . 8
β’ (π = suc π β (π₯ β ( O βπ) β π₯ β ( O βsuc π))) |
18 | 17 | rspcev 3583 |
. . . . . . 7
β’ ((suc
π β π΄ β§ π₯ β ( O βsuc π)) β βπ β π΄ π₯ β ( O βπ)) |
19 | 4, 15, 18 | syl2anc 585 |
. . . . . 6
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( M βπ))) β βπ β π΄ π₯ β ( O βπ)) |
20 | 19 | rexlimdvaa 3150 |
. . . . 5
β’ ((Lim
π΄ β§ π΄ β π) β (βπ β π΄ π₯ β ( M βπ) β βπ β π΄ π₯ β ( O βπ))) |
21 | | simprl 770 |
. . . . . . 7
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( O βπ))) β π β π΄) |
22 | | oldssmade 27236 |
. . . . . . . 8
β’ ( O
βπ) β ( M
βπ) |
23 | | simprr 772 |
. . . . . . . 8
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( O βπ))) β π₯ β ( O βπ)) |
24 | 22, 23 | sselid 3946 |
. . . . . . 7
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( O βπ))) β π₯ β ( M βπ)) |
25 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π β ( M βπ) = ( M βπ)) |
26 | 25 | eleq2d 2820 |
. . . . . . . 8
β’ (π = π β (π₯ β ( M βπ) β π₯ β ( M βπ))) |
27 | 26 | rspcev 3583 |
. . . . . . 7
β’ ((π β π΄ β§ π₯ β ( M βπ)) β βπ β π΄ π₯ β ( M βπ)) |
28 | 21, 24, 27 | syl2anc 585 |
. . . . . 6
β’ (((Lim
π΄ β§ π΄ β π) β§ (π β π΄ β§ π₯ β ( O βπ))) β βπ β π΄ π₯ β ( M βπ)) |
29 | 28 | rexlimdvaa 3150 |
. . . . 5
β’ ((Lim
π΄ β§ π΄ β π) β (βπ β π΄ π₯ β ( O βπ) β βπ β π΄ π₯ β ( M βπ))) |
30 | 20, 29 | impbid 211 |
. . . 4
β’ ((Lim
π΄ β§ π΄ β π) β (βπ β π΄ π₯ β ( M βπ) β βπ β π΄ π₯ β ( O βπ))) |
31 | | elold 27228 |
. . . . 5
β’ (π΄ β On β (π₯ β ( O βπ΄) β βπ β π΄ π₯ β ( M βπ))) |
32 | 10, 31 | syl 17 |
. . . 4
β’ ((Lim
π΄ β§ π΄ β π) β (π₯ β ( O βπ΄) β βπ β π΄ π₯ β ( M βπ))) |
33 | | eliun 4962 |
. . . . 5
β’ (π₯ β βͺ π β π΄ ( O βπ) β βπ β π΄ π₯ β ( O βπ)) |
34 | 33 | a1i 11 |
. . . 4
β’ ((Lim
π΄ β§ π΄ β π) β (π₯ β βͺ
π β π΄ ( O βπ) β βπ β π΄ π₯ β ( O βπ))) |
35 | 30, 32, 34 | 3bitr4d 311 |
. . 3
β’ ((Lim
π΄ β§ π΄ β π) β (π₯ β ( O βπ΄) β π₯ β βͺ
π β π΄ ( O βπ))) |
36 | 35 | eqrdv 2731 |
. 2
β’ ((Lim
π΄ β§ π΄ β π) β ( O βπ΄) = βͺ
π β π΄ ( O βπ)) |
37 | | oldf 27216 |
. . 3
β’ O
:OnβΆπ« No |
38 | | ffun 6675 |
. . 3
β’ ( O
:OnβΆπ« No β Fun O
) |
39 | | funiunfv 7199 |
. . 3
β’ (Fun O
β βͺ π β π΄ ( O βπ) = βͺ ( O β
π΄)) |
40 | 37, 38, 39 | mp2b 10 |
. 2
β’ βͺ π β π΄ ( O βπ) = βͺ ( O β
π΄) |
41 | 36, 40 | eqtrdi 2789 |
1
β’ ((Lim
π΄ β§ π΄ β π) β ( O βπ΄) = βͺ ( O β
π΄)) |