Step Hyp Ref
Expression 1 simpl 457 . . . 4
2 r1funlim 8205 . . . . . . . 8
3 2 simpri 462 . . . . . . 7
4 limord 4942 . . . . . . 7
5 3 , 4 ax-mp 5 . . . . . 6
6 ordsson 6625 . . . . . 6
7 5 , 6 ax-mp 5 . . . . 5
8 7 sseli 3499 . . . 4
9 1 , 8 syl 16 . . 3
10 onelon 4908 . . . . 5
11 8 , 10 sylan 471 . . . 4
12 suceloni 6648 . . . 4
13 11 , 12 syl 16 . . 3
14 eloni 4893 . . . . . 6
15 ordsucss 6653 . . . . . 6
16 14 , 15 syl 16 . . . . 5
17 16 imp 429 . . . 4
18 8 , 17 sylan 471 . . 3
19 eleq1 2529 . . . . . 6
20 fveq2 5871 . . . . . . 7
21 20 eleq2d 2527 . . . . . 6
22 19 , 21 imbi12d 320 . . . . 5
23 eleq1 2529 . . . . . 6
24 fveq2 5871 . . . . . . 7
25 24 eleq2d 2527 . . . . . 6
26 23 , 25 imbi12d 320 . . . . 5
27 eleq1 2529 . . . . . 6
28 fveq2 5871 . . . . . . 7
29 28 eleq2d 2527 . . . . . 6
30 27 , 29 imbi12d 320 . . . . 5
31 eleq1 2529 . . . . . 6
32 fveq2 5871 . . . . . . 7
33 32 eleq2d 2527 . . . . . 6
34 31 , 33 imbi12d 320 . . . . 5
35 fvex 5881 . . . . . . . 8
36 35 pwid 4026 . . . . . . 7
37 limsuc 6684 . . . . . . . . 9
38 3 , 37 ax-mp 5 . . . . . . . 8
39 r1sucg 8208 . . . . . . . 8
40 38 , 39 sylbir 213 . . . . . . 7
41 36 , 40 syl5eleqr 2552 . . . . . 6
42 41 a1i 11 . . . . 5
43 limsuc 6684 . . . . . . . 8
44 3 , 43 ax-mp 5 . . . . . . 7
45 r1tr 8215 . . . . . . . . . . 11
46 dftr4 4550 . . . . . . . . . . 11
47 45 , 46 mpbi 208 . . . . . . . . . 10
48 r1sucg 8208 . . . . . . . . . 10
49 47 , 48 syl5sseqr 3552 . . . . . . . . 9
50 49 sseld 3502 . . . . . . . 8
51 50 a2i 13 . . . . . . 7
52 44 , 51 syl5bir 218 . . . . . 6
53 52 a1i 11 . . . . 5
54 simprl 756 . . . . . . . . . . . 12
55 simplr 755 . . . . . . . . . . . . . 14
56 sucelon 6652 . . . . . . . . . . . . . 14
57 55 , 56 sylibr 212 . . . . . . . . . . . . 13
58 limord 4942 . . . . . . . . . . . . . 14
59 58 ad2antrr 725 . . . . . . . . . . . . 13
60 ordelsuc 6655 . . . . . . . . . . . . 13
61 57 , 59 , 60 syl2anc 661 . . . . . . . . . . . 12
62 54 , 61 mpbird 232 . . . . . . . . . . 11
63 limsuc 6684 . . . . . . . . . . . 12
64 63 ad2antrr 725 . . . . . . . . . . 11
65 62 , 64 mpbid 210 . . . . . . . . . 10
66 simprr 757 . . . . . . . . . . . . 13
67 ordtr1 4926 . . . . . . . . . . . . . 14
68 5 , 67 ax-mp 5 . . . . . . . . . . . . 13
69 62 , 66 , 68 syl2anc 661 . . . . . . . . . . . 12
70 69 , 39 syl 16 . . . . . . . . . . 11
71 36 , 70 syl5eleqr 2552 . . . . . . . . . 10
72 fveq2 5871 . . . . . . . . . . . 12
73 72 eleq2d 2527 . . . . . . . . . . 11
74 73 rspcev 3210 . . . . . . . . . 10
75 65 , 71 , 74 syl2anc 661 . . . . . . . . 9
76 eliun 4335 . . . . . . . . 9
77 75 , 76 sylibr 212 . . . . . . . 8
78 simpll 753 . . . . . . . . 9
79 r1limg 8210 . . . . . . . . 9
80 66 , 78 , 79 syl2anc 661 . . . . . . . 8
81 77 , 80 eleqtrrd 2548 . . . . . . 7
82 81 expr 615 . . . . . 6
83 82 a1d 25 . . . . 5
84 22 , 26 , 30 , 34 , 42 , 53 , 83 tfindsg 6695 . . . 4
85 84 impr 619 . . 3
86 9 , 13 , 18 , 1 , 85 syl22anc 1229 . 2
87 86 ex 434 1
