Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
2 | 1 | cbvmptv 5219 |
. . . . 5
β’ (π β π β¦ (πΉβπ)) = (π β π β¦ (πΉβπ)) |
3 | | caucvg.1 |
. . . . . . . . . 10
β’ π =
(β€β₯βπ) |
4 | | uzssz 12789 |
. . . . . . . . . 10
β’
(β€β₯βπ) β β€ |
5 | 3, 4 | eqsstri 3979 |
. . . . . . . . 9
β’ π β
β€ |
6 | | zssre 12511 |
. . . . . . . . 9
β’ β€
β β |
7 | 5, 6 | sstri 3954 |
. . . . . . . 8
β’ π β
β |
8 | 7 | a1i 11 |
. . . . . . 7
β’ (π β π β β) |
9 | | caucvg.2 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) β β) |
10 | 2 | eqcomi 2742 |
. . . . . . . 8
β’ (π β π β¦ (πΉβπ)) = (π β π β¦ (πΉβπ)) |
11 | 9, 10 | fmptd 7063 |
. . . . . . 7
β’ (π β (π β π β¦ (πΉβπ)):πβΆβ) |
12 | | 1rp 12924 |
. . . . . . . . . . 11
β’ 1 β
β+ |
13 | 12 | ne0ii 4298 |
. . . . . . . . . 10
β’
β+ β β
|
14 | | caucvg.3 |
. . . . . . . . . 10
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) |
15 | | r19.2z 4453 |
. . . . . . . . . 10
β’
((β+ β β
β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) |
16 | 13, 14, 15 | sylancr 588 |
. . . . . . . . 9
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) |
17 | | eluzel2 12773 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β π β β€) |
18 | 17, 3 | eleq2s 2852 |
. . . . . . . . . . . 12
β’ (π β π β π β β€) |
19 | 18 | a1d 25 |
. . . . . . . . . . 11
β’ (π β π β (βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β π β β€)) |
20 | 19 | rexlimiv 3142 |
. . . . . . . . . 10
β’
(βπ β
π βπ β
(β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β π β β€) |
21 | 20 | rexlimivw 3145 |
. . . . . . . . 9
β’
(βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β π β β€) |
22 | 16, 21 | syl 17 |
. . . . . . . 8
β’ (π β π β β€) |
23 | 3 | uzsup 13774 |
. . . . . . . 8
β’ (π β β€ β sup(π, β*, < ) =
+β) |
24 | 22, 23 | syl 17 |
. . . . . . 7
β’ (π β sup(π, β*, < ) =
+β) |
25 | 5 | sseli 3941 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π β β€) |
26 | 5 | sseli 3941 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π β β€) |
27 | | eluz 12782 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β€) β (π β
(β€β₯βπ) β π β€ π)) |
28 | 25, 26, 27 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π) β (π β (β€β₯βπ) β π β€ π)) |
29 | 28 | biimprd 248 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β (π β€ π β π β (β€β₯βπ))) |
30 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΉβπ) = (πΉβπ)) |
31 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β¦ (πΉβπ)) = (π β π β¦ (πΉβπ)) |
32 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉβπ) β V |
33 | 30, 31, 32 | fvmpt3i 6954 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β ((π β π β¦ (πΉβπ))βπ) = (πΉβπ)) |
34 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΉβπ) = (πΉβπ)) |
35 | 34, 31, 32 | fvmpt3i 6954 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β ((π β π β¦ (πΉβπ))βπ) = (πΉβπ)) |
36 | 33, 35 | oveqan12rd 7378 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ π β π) β (((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ)) = ((πΉβπ) β (πΉβπ))) |
37 | 36 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β π) β (absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) = (absβ((πΉβπ) β (πΉβπ)))) |
38 | 37 | breq1d 5116 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π) β ((absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) < π₯ β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
39 | 38 | biimprd 248 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β ((absβ((πΉβπ) β (πΉβπ))) < π₯ β (absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) < π₯)) |
40 | 29, 39 | imim12d 81 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π) β ((π β (β€β₯βπ) β (absβ((πΉβπ) β (πΉβπ))) < π₯) β (π β€ π β (absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) < π₯))) |
41 | 40 | ex 414 |
. . . . . . . . . . . 12
β’ (π β π β (π β π β ((π β (β€β₯βπ) β (absβ((πΉβπ) β (πΉβπ))) < π₯) β (π β€ π β (absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) < π₯)))) |
42 | 41 | com23 86 |
. . . . . . . . . . 11
β’ (π β π β ((π β (β€β₯βπ) β (absβ((πΉβπ) β (πΉβπ))) < π₯) β (π β π β (π β€ π β (absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) < π₯)))) |
43 | 42 | ralimdv2 3157 |
. . . . . . . . . 10
β’ (π β π β (βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β βπ β π (π β€ π β (absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) < π₯))) |
44 | 43 | reximia 3081 |
. . . . . . . . 9
β’
(βπ β
π βπ β
(β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β βπ β π βπ β π (π β€ π β (absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) < π₯)) |
45 | 44 | ralimi 3083 |
. . . . . . . 8
β’
(βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β βπ₯ β β+ βπ β π βπ β π (π β€ π β (absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) < π₯)) |
46 | 14, 45 | syl 17 |
. . . . . . 7
β’ (π β βπ₯ β β+ βπ β π βπ β π (π β€ π β (absβ(((π β π β¦ (πΉβπ))βπ) β ((π β π β¦ (πΉβπ))βπ))) < π₯)) |
47 | 8, 11, 24, 46 | caucvgr 15566 |
. . . . . 6
β’ (π β (π β π β¦ (πΉβπ)) β dom βπ
) |
48 | 11, 24 | rlimdm 15439 |
. . . . . 6
β’ (π β ((π β π β¦ (πΉβπ)) β dom βπ
β (π β π β¦ (πΉβπ)) βπ (
βπ β(π β π β¦ (πΉβπ))))) |
49 | 47, 48 | mpbid 231 |
. . . . 5
β’ (π β (π β π β¦ (πΉβπ)) βπ (
βπ β(π β π β¦ (πΉβπ)))) |
50 | 2, 49 | eqbrtrid 5141 |
. . . 4
β’ (π β (π β π β¦ (πΉβπ)) βπ (
βπ β(π β π β¦ (πΉβπ)))) |
51 | | eqid 2733 |
. . . . . 6
β’ (π β π β¦ (πΉβπ)) = (π β π β¦ (πΉβπ)) |
52 | 9, 51 | fmptd 7063 |
. . . . 5
β’ (π β (π β π β¦ (πΉβπ)):πβΆβ) |
53 | 3, 22, 52 | rlimclim 15434 |
. . . 4
β’ (π β ((π β π β¦ (πΉβπ)) βπ (
βπ β(π β π β¦ (πΉβπ))) β (π β π β¦ (πΉβπ)) β ( βπ
β(π β π β¦ (πΉβπ))))) |
54 | 50, 53 | mpbid 231 |
. . 3
β’ (π β (π β π β¦ (πΉβπ)) β ( βπ
β(π β π β¦ (πΉβπ)))) |
55 | | caucvg.4 |
. . . 4
β’ (π β πΉ β π) |
56 | 3, 51 | climmpt 15459 |
. . . 4
β’ ((π β β€ β§ πΉ β π) β (πΉ β ( βπ
β(π β π β¦ (πΉβπ))) β (π β π β¦ (πΉβπ)) β ( βπ
β(π β π β¦ (πΉβπ))))) |
57 | 22, 55, 56 | syl2anc 585 |
. . 3
β’ (π β (πΉ β ( βπ
β(π β π β¦ (πΉβπ))) β (π β π β¦ (πΉβπ)) β ( βπ
β(π β π β¦ (πΉβπ))))) |
58 | 54, 57 | mpbird 257 |
. 2
β’ (π β πΉ β ( βπ
β(π β π β¦ (πΉβπ)))) |
59 | | climrel 15380 |
. . 3
β’ Rel
β |
60 | 59 | releldmi 5904 |
. 2
β’ (πΉ β (
βπ β(π β π β¦ (πΉβπ))) β πΉ β dom β ) |
61 | 58, 60 | syl 17 |
1
β’ (π β πΉ β dom β ) |