Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . 4
β’
β²ππ |
2 | | smflimsuplem4.m |
. . . 4
β’ (π β π β β€) |
3 | | smflimsuplem4.z |
. . . . 5
β’ π =
(β€β₯βπ) |
4 | | smflimsuplem4.n |
. . . . 5
β’ (π β π β π) |
5 | 3, 4 | eluzelz2d 43738 |
. . . 4
β’ (π β π β β€) |
6 | | eqid 2733 |
. . . 4
β’
(β€β₯βπ) = (β€β₯βπ) |
7 | | fvexd 6861 |
. . . 4
β’ ((π β§ π β π) β ((πΉβπ)βπ₯) β V) |
8 | | fvexd 6861 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((πΉβπ)βπ₯) β V) |
9 | 1, 2, 5, 3, 6, 7, 8 | limsupequzmpt 44060 |
. . 3
β’ (π β (lim supβ(π β π β¦ ((πΉβπ)βπ₯))) = (lim supβ(π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)))) |
10 | | smflimsuplem4.s |
. . . . . . . 8
β’ (π β π β SAlg) |
11 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β π β SAlg) |
12 | 3, 4 | uzssd2 43742 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π) |
13 | 12 | sselda 3948 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β π β π) |
14 | | smflimsuplem4.f |
. . . . . . . . 9
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
15 | 14 | ffvelcdmda 7039 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
16 | 13, 15 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β (SMblFnβπ)) |
17 | | eqid 2733 |
. . . . . . 7
β’ dom
(πΉβπ) = dom (πΉβπ) |
18 | 11, 16, 17 | smff 45063 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ):dom (πΉβπ)βΆβ) |
19 | | smflimsuplem4.e |
. . . . . . . 8
β’ πΈ = (π β π β¦ {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
20 | | smflimsuplem4.h |
. . . . . . . 8
β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
))) |
21 | 3, 19, 20, 13 | smflimsuplem1 45151 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β dom (π»βπ) β dom (πΉβπ)) |
22 | | smflimsuplem4.i |
. . . . . . . . 9
β’ (π β π₯ β β©
π β
(β€β₯βπ)dom (π»βπ)) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β π₯ β β©
π β
(β€β₯βπ)dom (π»βπ)) |
24 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
25 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = π β (π»βπ) = (π»βπ)) |
26 | 25 | dmeqd 5865 |
. . . . . . . . 9
β’ (π = π β dom (π»βπ) = dom (π»βπ)) |
27 | 26 | eleq2d 2820 |
. . . . . . . 8
β’ (π = π β (π₯ β dom (π»βπ) β π₯ β dom (π»βπ))) |
28 | 23, 24, 27 | eliind 43371 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β π₯ β dom (π»βπ)) |
29 | 21, 28 | sseldd 3949 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π₯ β dom (πΉβπ)) |
30 | 18, 29 | ffvelcdmd 7040 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β ((πΉβπ)βπ₯) β β) |
31 | 30 | rexrd 11213 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((πΉβπ)βπ₯) β
β*) |
32 | 1, 5, 6, 31 | limsupvaluzmpt 44048 |
. . 3
β’ (π β (lim supβ(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯))) = inf(ran (π β (β€β₯βπ) β¦ sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )),
β*, < )) |
33 | 9, 32 | eqtrd 2773 |
. 2
β’ (π β (lim supβ(π β π β¦ ((πΉβπ)βπ₯))) = inf(ran (π β (β€β₯βπ) β¦ sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )),
β*, < )) |
34 | | smflimsuplem4.1 |
. . 3
β’
β²ππ |
35 | 12 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β
(β€β₯βπ) β π) |
36 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
37 | 35, 36 | sseldd 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β π β π) |
38 | 20 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
)))) |
39 | | fvex 6859 |
. . . . . . . . . . . . . . 15
β’ (πΈβπ) β V |
40 | 39 | mptex 7177 |
. . . . . . . . . . . . . 14
β’ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) β
V |
41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) β
V) |
42 | 38, 41 | fvmpt2d 6965 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π»βπ) = (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
))) |
43 | 37, 42 | syldan 592 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β (π»βπ) = (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
))) |
44 | 43 | dmeqd 5865 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β dom (π»βπ) = dom (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
))) |
45 | | xrltso 13069 |
. . . . . . . . . . . . 13
β’ < Or
β* |
46 | 45 | supex 9407 |
. . . . . . . . . . . 12
β’ sup(ran
(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
V |
47 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) = (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
)) |
48 | 46, 47 | dmmpti 6649 |
. . . . . . . . . . 11
β’ dom
(π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) = (πΈβπ) |
49 | 48 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β dom (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) = (πΈβπ)) |
50 | 44, 49 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β dom (π»βπ) = (πΈβπ)) |
51 | 34, 50 | iineq2d 4981 |
. . . . . . . 8
β’ (π β β© π β (β€β₯βπ)dom (π»βπ) = β© π β
(β€β₯βπ)(πΈβπ)) |
52 | 22, 51 | eleqtrd 2836 |
. . . . . . 7
β’ (π β π₯ β β©
π β
(β€β₯βπ)(πΈβπ)) |
53 | 52 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π₯ β β©
π β
(β€β₯βπ)(πΈβπ)) |
54 | | eliinid 43413 |
. . . . . 6
β’ ((π₯ β β© π β (β€β₯βπ)(πΈβπ) β§ π β (β€β₯βπ)) β π₯ β (πΈβπ)) |
55 | 53, 36, 54 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β π₯ β (πΈβπ)) |
56 | 46 | a1i 11 |
. . . . . 6
β’ (((π β§ π β (β€β₯βπ)) β§ π₯ β (πΈβπ)) β sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
V) |
57 | 43, 56 | fvmpt2d 6965 |
. . . . 5
β’ (((π β§ π β (β€β₯βπ)) β§ π₯ β (πΈβπ)) β ((π»βπ)βπ₯) = sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
)) |
58 | 55, 57 | mpdan 686 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((π»βπ)βπ₯) = sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
)) |
59 | | eqid 2733 |
. . . . . . . . . 10
β’ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} = {π₯ β
β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} |
60 | 3 | eluzelz2 43728 |
. . . . . . . . . . . . 13
β’ (π β π β π β β€) |
61 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(β€β₯βπ) = (β€β₯βπ) |
62 | 60, 61 | uzn0d 43750 |
. . . . . . . . . . . 12
β’ (π β π β (β€β₯βπ) β β
) |
63 | | fvex 6859 |
. . . . . . . . . . . . . . 15
β’ (πΉβπ) β V |
64 | 63 | dmex 7852 |
. . . . . . . . . . . . . 14
β’ dom
(πΉβπ) β V |
65 | 64 | rgenw 3065 |
. . . . . . . . . . . . 13
β’
βπ β
(β€β₯βπ)dom (πΉβπ) β V |
66 | 65 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β π β βπ β (β€β₯βπ)dom (πΉβπ) β V) |
67 | 62, 66 | iinexd 43435 |
. . . . . . . . . . 11
β’ (π β π β β©
π β
(β€β₯βπ)dom (πΉβπ) β V) |
68 | 67 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β π) β β©
π β
(β€β₯βπ)dom (πΉβπ) β V) |
69 | 59, 68 | rabexd 5294 |
. . . . . . . . 9
β’ ((π β§ π β π) β {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} β V) |
70 | 37, 69 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} β V) |
71 | 19 | fvmpt2 6963 |
. . . . . . . 8
β’ ((π β π β§ {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} β V) β (πΈβπ) = {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
72 | 37, 70, 71 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (πΈβπ) = {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
73 | 55, 72 | eleqtrd 2836 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π₯ β {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
74 | | rabid 3426 |
. . . . . 6
β’ (π₯ β {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} β (π₯ β
β© π β (β€β₯βπ)dom (πΉβπ) β§ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β)) |
75 | 73, 74 | sylib 217 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β (π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β§ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β)) |
76 | 75 | simprd 497 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β) |
77 | 58, 76 | eqeltrd 2834 |
. . 3
β’ ((π β§ π β (β€β₯βπ)) β ((π»βπ)βπ₯) β β) |
78 | 34, 58 | mpteq2da 5207 |
. . . 4
β’ (π β (π β (β€β₯βπ) β¦ ((π»βπ)βπ₯)) = (π β (β€β₯βπ) β¦ sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
))) |
79 | | nfv 1918 |
. . . . 5
β’
β²ππ |
80 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
81 | 80 | mpteq1d 5204 |
. . . . . . 7
β’ (π = π β (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) = (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯))) |
82 | 81 | rneqd 5897 |
. . . . . 6
β’ (π = π β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) = ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯))) |
83 | 82 | supeq1d 9390 |
. . . . 5
β’ (π = π β sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) = sup(ran
(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
)) |
84 | | nfv 1918 |
. . . . . . . 8
β’
β²π(π β
(β€β₯βπ) β§ π = (π + 1)) |
85 | | eluzelz 12781 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β π β β€) |
86 | 85 | adantr 482 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β π β β€) |
87 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β π = (π + 1)) |
88 | 86 | peano2zd 12618 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β (π + 1) β β€) |
89 | 87, 88 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β π β β€) |
90 | 86 | zred 12615 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β π β β) |
91 | 89 | zred 12615 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β π β β) |
92 | 90 | ltp1d 12093 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β π < (π + 1)) |
93 | 87 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β (π + 1) = π) |
94 | 92, 93 | breqtrd 5135 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β π < π) |
95 | 90, 91, 94 | ltled 11311 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β π β€ π) |
96 | 61, 86, 89, 95 | eluzd 43734 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β π β (β€β₯βπ)) |
97 | | uzss 12794 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
98 | 96, 97 | syl 17 |
. . . . . . . 8
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β
(β€β₯βπ) β (β€β₯βπ)) |
99 | | fvexd 6861 |
. . . . . . . 8
β’ (((π β
(β€β₯βπ) β§ π = (π + 1)) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ₯) β V) |
100 | 84, 98, 99 | rnmptss2 43576 |
. . . . . . 7
β’ ((π β
(β€β₯βπ) β§ π = (π + 1)) β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯))) |
101 | 100 | 3adant1 1131 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ) β§ π = (π + 1)) β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯))) |
102 | | nfv 1918 |
. . . . . . . . 9
β’
β²π(π β§ π β (β€β₯βπ)) |
103 | | eqid 2733 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) = (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) |
104 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
105 | 37, 104 | syldanl 603 |
. . . . . . . . . 10
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β π) |
106 | 6 | uztrn2 12790 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
107 | 106 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
108 | 105, 107,
30 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ₯) β β) |
109 | 102, 103,
108 | rnmptssd 43508 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β β) |
110 | | ressxr 11207 |
. . . . . . . . 9
β’ β
β β* |
111 | 110 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β β β
β*) |
112 | 109, 111 | sstrd 3958 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β
β*) |
113 | 112 | 3adant3 1133 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ) β§ π = (π + 1)) β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β
β*) |
114 | | supxrss 13260 |
. . . . . 6
β’ ((ran
(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β§ ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) β β*) β
sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β€ sup(ran
(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
)) |
115 | 101, 113,
114 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ) β§ π = (π + 1)) β sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β€ sup(ran
(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
)) |
116 | | smflimsuplem4.c |
. . . . . . 7
β’ (π β (π β π β¦ ((π»βπ)βπ₯)) β dom β ) |
117 | 3 | fvexi 6860 |
. . . . . . . . 9
β’ π β V |
118 | 117 | a1i 11 |
. . . . . . . 8
β’ (π β π β V) |
119 | | fvexd 6861 |
. . . . . . . 8
β’ ((π β§ π β π) β ((π»βπ)βπ₯) β V) |
120 | | fvexd 6861 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β V) |
121 | 34, 36 | ssdf 43377 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β
(β€β₯βπ)) |
122 | | fvexd 6861 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β ((π»βπ)βπ₯) β V) |
123 | | eqidd 2734 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β ((π»βπ)βπ₯) = ((π»βπ)βπ₯)) |
124 | 34, 5, 6, 118, 12, 119, 120, 121, 122, 123 | climeldmeqmpt 43999 |
. . . . . . 7
β’ (π β ((π β π β¦ ((π»βπ)βπ₯)) β dom β β (π β
(β€β₯βπ) β¦ ((π»βπ)βπ₯)) β dom β )) |
125 | 116, 124 | mpbid 231 |
. . . . . 6
β’ (π β (π β (β€β₯βπ) β¦ ((π»βπ)βπ₯)) β dom β ) |
126 | 78, 125 | eqeltrrd 2835 |
. . . . 5
β’ (π β (π β (β€β₯βπ) β¦ sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) β dom
β ) |
127 | 34, 79, 5, 6, 76, 83, 115, 126 | climinf2mpt 44045 |
. . . 4
β’ (π β (π β (β€β₯βπ) β¦ sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) β
inf(ran (π β
(β€β₯βπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )),
β*, < )) |
128 | 78, 127 | eqbrtrd 5131 |
. . 3
β’ (π β (π β (β€β₯βπ) β¦ ((π»βπ)βπ₯)) β inf(ran (π β (β€β₯βπ) β¦ sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )),
β*, < )) |
129 | 34, 5, 6, 77, 128 | climreclmpt 44015 |
. 2
β’ (π β inf(ran (π β
(β€β₯βπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )),
β*, < ) β β) |
130 | 33, 129 | eqeltrd 2834 |
1
β’ (π β (lim supβ(π β π β¦ ((πΉβπ)βπ₯))) β β) |