Step | Hyp | Ref
| Expression |
1 | | elioore 13300 |
. . . . . . 7
β’ ((πΉβπ) β ((π΄ β 1)(,)(π΄ + 1)) β (πΉβπ) β β) |
2 | 1 | anim2i 618 |
. . . . . 6
β’ ((π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1))) β (π β dom πΉ β§ (πΉβπ) β β)) |
3 | 2 | ralimi 3083 |
. . . . 5
β’
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1))) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β)) |
4 | 3 | adantl 483 |
. . . 4
β’ ((π β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1)))) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β)) |
5 | | xlimxrre.f |
. . . . . . 7
β’ (π β πΉ:πβΆβ*) |
6 | 5 | ffund 6673 |
. . . . . 6
β’ (π β Fun πΉ) |
7 | | ffvresb 7073 |
. . . . . 6
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
8 | 6, 7 | syl 17 |
. . . . 5
β’ (π β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
9 | 8 | adantr 482 |
. . . 4
β’ ((π β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1)))) β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
10 | 4, 9 | mpbird 257 |
. . 3
β’ ((π β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1)))) β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
11 | 10 | adantrl 715 |
. 2
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1))))) β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
12 | | xlimxrre.a |
. . . . . 6
β’ (π β π΄ β β) |
13 | | peano2rem 11473 |
. . . . . 6
β’ (π΄ β β β (π΄ β 1) β
β) |
14 | 12, 13 | syl 17 |
. . . . 5
β’ (π β (π΄ β 1) β β) |
15 | 14 | rexrd 11210 |
. . . 4
β’ (π β (π΄ β 1) β
β*) |
16 | | peano2re 11333 |
. . . . . 6
β’ (π΄ β β β (π΄ + 1) β
β) |
17 | 12, 16 | syl 17 |
. . . . 5
β’ (π β (π΄ + 1) β β) |
18 | 17 | rexrd 11210 |
. . . 4
β’ (π β (π΄ + 1) β
β*) |
19 | 12 | ltm1d 12092 |
. . . 4
β’ (π β (π΄ β 1) < π΄) |
20 | 12 | ltp1d 12090 |
. . . 4
β’ (π β π΄ < (π΄ + 1)) |
21 | 15, 18, 12, 19, 20 | eliood 43822 |
. . 3
β’ (π β π΄ β ((π΄ β 1)(,)(π΄ + 1))) |
22 | | iooordt 22584 |
. . . 4
β’ ((π΄ β 1)(,)(π΄ + 1)) β (ordTopβ β€
) |
23 | | xlimxrre.c |
. . . . . 6
β’ (π β πΉ~~>*π΄) |
24 | | nfcv 2904 |
. . . . . . 7
β’
β²ππΉ |
25 | | xlimxrre.m |
. . . . . . 7
β’ (π β π β β€) |
26 | | xlimxrre.z |
. . . . . . 7
β’ π =
(β€β₯βπ) |
27 | | eqid 2733 |
. . . . . . 7
β’
(ordTopβ β€ ) = (ordTopβ β€ ) |
28 | 24, 25, 26, 5, 27 | xlimbr 44154 |
. . . . . 6
β’ (π β (πΉ~~>*π΄ β (π΄ β β* β§
βπ’ β
(ordTopβ β€ )(π΄
β π’ β
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
29 | 23, 28 | mpbid 231 |
. . . . 5
β’ (π β (π΄ β β* β§
βπ’ β
(ordTopβ β€ )(π΄
β π’ β
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
30 | 29 | simprd 497 |
. . . 4
β’ (π β βπ’ β (ordTopβ β€ )(π΄ β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
31 | | eleq2 2823 |
. . . . . 6
β’ (π’ = ((π΄ β 1)(,)(π΄ + 1)) β (π΄ β π’ β π΄ β ((π΄ β 1)(,)(π΄ + 1)))) |
32 | | eleq2 2823 |
. . . . . . . 8
β’ (π’ = ((π΄ β 1)(,)(π΄ + 1)) β ((πΉβπ) β π’ β (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1)))) |
33 | 32 | anbi2d 630 |
. . . . . . 7
β’ (π’ = ((π΄ β 1)(,)(π΄ + 1)) β ((π β dom πΉ β§ (πΉβπ) β π’) β (π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1))))) |
34 | 33 | rexralbidv 3211 |
. . . . . 6
β’ (π’ = ((π΄ β 1)(,)(π΄ + 1)) β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1))))) |
35 | 31, 34 | imbi12d 345 |
. . . . 5
β’ (π’ = ((π΄ β 1)(,)(π΄ + 1)) β ((π΄ β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β (π΄ β ((π΄ β 1)(,)(π΄ + 1)) β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1)))))) |
36 | 35 | rspcva 3578 |
. . . 4
β’ ((((π΄ β 1)(,)(π΄ + 1)) β (ordTopβ β€ ) β§
βπ’ β
(ordTopβ β€ )(π΄
β π’ β
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) β (π΄ β ((π΄ β 1)(,)(π΄ + 1)) β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1))))) |
37 | 22, 30, 36 | sylancr 588 |
. . 3
β’ (π β (π΄ β ((π΄ β 1)(,)(π΄ + 1)) β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1))))) |
38 | 21, 37 | mpd 15 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β ((π΄ β 1)(,)(π΄ + 1)))) |
39 | 11, 38 | reximddv 3165 |
1
β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |