Step | Hyp | Ref
| Expression |
1 | | smflimsuplem5.a |
. . 3
β’
β²ππ |
2 | | smflimsuplem5.n |
. . . . . . . 8
β’ (π β π β π) |
3 | | smflimsuplem5.z |
. . . . . . . . . . . 12
β’ π =
(β€β₯βπ) |
4 | 3 | eleq2i 2824 |
. . . . . . . . . . 11
β’ (π β π β π β (β€β₯βπ)) |
5 | 4 | biimpi 215 |
. . . . . . . . . 10
β’ (π β π β π β (β€β₯βπ)) |
6 | | uzss 12810 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
β’ (π β π β (β€β₯βπ) β
(β€β₯βπ)) |
8 | 7, 3 | sseqtrrdi 4013 |
. . . . . . . 8
β’ (π β π β (β€β₯βπ) β π) |
9 | 2, 8 | syl 17 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β π) |
10 | 9 | sselda 3962 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π β π) |
11 | | smflimsuplem5.e |
. . . . . . . . . 10
β’ πΈ = (π β π β¦ {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
12 | | nfcv 2902 |
. . . . . . . . . . 11
β’
β²π₯π |
13 | | nfrab1 3437 |
. . . . . . . . . . 11
β’
β²π₯{π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} |
14 | 12, 13 | nfmpt 5232 |
. . . . . . . . . 10
β’
β²π₯(π β π β¦ {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
15 | 11, 14 | nfcxfr 2900 |
. . . . . . . . 9
β’
β²π₯πΈ |
16 | | nfcv 2902 |
. . . . . . . . 9
β’
β²π₯π |
17 | 15, 16 | nffv 6872 |
. . . . . . . 8
β’
β²π₯(πΈβπ) |
18 | | fvex 6875 |
. . . . . . . 8
β’ (πΈβπ) β V |
19 | 17, 18 | mptexf 43617 |
. . . . . . 7
β’ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) β
V |
20 | 19 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) β
V) |
21 | | smflimsuplem5.h |
. . . . . . 7
β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
))) |
22 | 21 | fvmpt2 6979 |
. . . . . 6
β’ ((π β π β§ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) β V)
β (π»βπ) = (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
))) |
23 | 10, 20, 22 | syl2anc 584 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β (π»βπ) = (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
))) |
24 | 23 | fveq1d 6864 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((π»βπ)βπ) = ((π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))βπ)) |
25 | | nfcv 2902 |
. . . . . 6
β’
β²π¦(πΈβπ) |
26 | | nfcv 2902 |
. . . . . 6
β’
β²π¦sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
) |
27 | | nfcv 2902 |
. . . . . 6
β’
β²π₯sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)), β*, <
) |
28 | | fveq2 6862 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((πΉβπ)βπ₯) = ((πΉβπ)βπ¦)) |
29 | 28 | mpteq2dv 5227 |
. . . . . . . 8
β’ (π₯ = π¦ β (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) = (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦))) |
30 | 29 | rneqd 5913 |
. . . . . . 7
β’ (π₯ = π¦ β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)) = ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦))) |
31 | 30 | supeq1d 9406 |
. . . . . 6
β’ (π₯ = π¦ β sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) = sup(ran
(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ¦)), β*, <
)) |
32 | 17, 25, 26, 27, 31 | cbvmptf 5234 |
. . . . 5
β’ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < )) = (π¦ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)), β*, <
)) |
33 | | simpl 483 |
. . . . . . . . 9
β’ ((π¦ = π β§ π β (β€β₯βπ)) β π¦ = π) |
34 | 33 | fveq2d 6866 |
. . . . . . . 8
β’ ((π¦ = π β§ π β (β€β₯βπ)) β ((πΉβπ)βπ¦) = ((πΉβπ)βπ)) |
35 | 34 | mpteq2dva 5225 |
. . . . . . 7
β’ (π¦ = π β (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)) = (π β (β€β₯βπ) β¦ ((πΉβπ)βπ))) |
36 | 35 | rneqd 5913 |
. . . . . 6
β’ (π¦ = π β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)) = ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ))) |
37 | 36 | supeq1d 9406 |
. . . . 5
β’ (π¦ = π β sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)), β*, < ) = sup(ran
(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)), β*, <
)) |
38 | 37 | eleq1d 2817 |
. . . . . . . 8
β’ (π¦ = π β (sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)), β*, < ) β
β β sup(ran (π
β (β€β₯βπ) β¦ ((πΉβπ)βπ)), β*, < ) β
β)) |
39 | | uzss 12810 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
40 | | iinss1 4989 |
. . . . . . . . . . 11
β’
((β€β₯βπ) β (β€β₯βπ) β β© π β (β€β₯βπ)dom (πΉβπ) β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β β©
π β
(β€β₯βπ)dom (πΉβπ) β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
42 | 41 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β β© π β (β€β₯βπ)dom (πΉβπ) β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
43 | | smflimsuplem5.x |
. . . . . . . . . 10
β’ (π β π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
44 | 43 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
45 | 42, 44 | sseldd 3963 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β π β β©
π β
(β€β₯βπ)dom (πΉβπ)) |
46 | | smflimsuplem5.b |
. . . . . . . . . . 11
β’
β²ππ |
47 | | nfv 1917 |
. . . . . . . . . . 11
β’
β²π π β
(β€β₯βπ) |
48 | 46, 47 | nfan 1902 |
. . . . . . . . . 10
β’
β²π(π β§ π β (β€β₯βπ)) |
49 | | eqid 2731 |
. . . . . . . . . 10
β’
(β€β₯βπ) = (β€β₯βπ) |
50 | | simpll 765 |
. . . . . . . . . . 11
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β π) |
51 | 39 | sselda 3962 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
52 | 51 | adantll 712 |
. . . . . . . . . . 11
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
53 | | smflimsuplem5.s |
. . . . . . . . . . . . . 14
β’ (π β π β SAlg) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β π β SAlg) |
55 | | simpl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯βπ)) β π) |
56 | 9 | sselda 3962 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯βπ)) β π β π) |
57 | | smflimsuplem5.f |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
58 | 57 | ffvelcdmda 7055 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
59 | 55, 56, 58 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β (SMblFnβπ)) |
60 | | eqid 2731 |
. . . . . . . . . . . . 13
β’ dom
(πΉβπ) = dom (πΉβπ) |
61 | 54, 59, 60 | smff 45126 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ):dom (πΉβπ)βΆβ) |
62 | | eliin 4979 |
. . . . . . . . . . . . . . . 16
β’ (π β β© π β (β€β₯βπ)dom (πΉβπ) β (π β β©
π β
(β€β₯βπ)dom (πΉβπ) β βπ β (β€β₯βπ)π β dom (πΉβπ))) |
63 | 43, 62 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π β β©
π β
(β€β₯βπ)dom (πΉβπ) β βπ β (β€β₯βπ)π β dom (πΉβπ))) |
64 | 43, 63 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π β βπ β (β€β₯βπ)π β dom (πΉβπ)) |
65 | 64 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β βπ β
(β€β₯βπ)π β dom (πΉβπ)) |
66 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
67 | | rspa 3242 |
. . . . . . . . . . . . 13
β’
((βπ β
(β€β₯βπ)π β dom (πΉβπ) β§ π β (β€β₯βπ)) β π β dom (πΉβπ)) |
68 | 65, 66, 67 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β π β dom (πΉβπ)) |
69 | 61, 68 | ffvelcdmd 7056 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) β β) |
70 | 50, 52, 69 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) β β) |
71 | | eluzelz 12797 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β π β β€) |
72 | 71 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β π β β€) |
73 | | smflimsuplem5.m |
. . . . . . . . . . . . . 14
β’ (π β π β β€) |
74 | 73 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β π β β€) |
75 | | fvex 6875 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ)βπ) β V |
76 | 75 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯βπ)) β§ π β π) β ((πΉβπ)βπ) β V) |
77 | 48, 72, 74, 49, 3, 70, 76 | limsupequzmpt 44123 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β (lim supβ(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ))) = (lim supβ(π β π β¦ ((πΉβπ)βπ)))) |
78 | | smflimsuplem5.r |
. . . . . . . . . . . . 13
β’ (π β (lim supβ(π β π β¦ ((πΉβπ)βπ))) β β) |
79 | 78 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β (lim supβ(π β π β¦ ((πΉβπ)βπ))) β β) |
80 | 77, 79 | eqeltrd 2832 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯βπ)) β (lim supβ(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ))) β β) |
81 | 80 | renepnfd 11230 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β (lim supβ(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ))) β +β) |
82 | 48, 49, 70, 81 | limsupubuzmpt 44113 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β βπ¦ β β βπ β
(β€β₯βπ)((πΉβπ)βπ) β€ π¦) |
83 | | uzid2 43793 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β π β (β€β₯βπ)) |
84 | 83 | ne0d 4315 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β β
) |
85 | 84 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β
(β€β₯βπ) β β
) |
86 | 48, 85, 70 | supxrre3rnmpt 43817 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β (sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)), β*, < ) β
β β βπ¦
β β βπ
β (β€β₯βπ)((πΉβπ)βπ) β€ π¦)) |
87 | 82, 86 | mpbird 256 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)), β*, < ) β
β) |
88 | 38, 45, 87 | elrabd 3665 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β π β {π¦ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)), β*, < ) β
β}) |
89 | | simpl 483 |
. . . . . . . . . . . . 13
β’ ((π¦ = π₯ β§ π β (β€β₯βπ)) β π¦ = π₯) |
90 | 89 | fveq2d 6866 |
. . . . . . . . . . . 12
β’ ((π¦ = π₯ β§ π β (β€β₯βπ)) β ((πΉβπ)βπ¦) = ((πΉβπ)βπ₯)) |
91 | 90 | mpteq2dva 5225 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)) = (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯))) |
92 | 91 | rneqd 5913 |
. . . . . . . . . 10
β’ (π¦ = π₯ β ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)) = ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯))) |
93 | 92 | supeq1d 9406 |
. . . . . . . . 9
β’ (π¦ = π₯ β sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)), β*, < ) = sup(ran
(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, <
)) |
94 | 93 | eleq1d 2817 |
. . . . . . . 8
β’ (π¦ = π₯ β (sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)), β*, < ) β
β β sup(ran (π
β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β)) |
95 | 94 | cbvrabv 3428 |
. . . . . . 7
β’ {π¦ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ¦)), β*, < ) β
β} = {π₯ β
β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} |
96 | 88, 95 | eleqtrdi 2842 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π β {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
97 | | eqid 2731 |
. . . . . . . 8
β’ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} = {π₯ β
β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} |
98 | | fvex 6875 |
. . . . . . . . . . . . 13
β’ (πΉβπ) β V |
99 | 98 | dmex 7868 |
. . . . . . . . . . . 12
β’ dom
(πΉβπ) β V |
100 | 99 | rgenw 3064 |
. . . . . . . . . . 11
β’
βπ β
(β€β₯βπ)dom (πΉβπ) β V |
101 | 100 | a1i 11 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β βπ β (β€β₯βπ)dom (πΉβπ) β V) |
102 | 84, 101 | iinexd 43498 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β β©
π β
(β€β₯βπ)dom (πΉβπ) β V) |
103 | 102 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯βπ)) β β© π β (β€β₯βπ)dom (πΉβπ) β V) |
104 | 97, 103 | rabexd 5310 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} β V) |
105 | 11 | fvmpt2 6979 |
. . . . . . 7
β’ ((π β π β§ {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β} β V) β (πΈβπ) = {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
106 | 10, 104, 105 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β (πΈβπ) = {π₯ β β©
π β
(β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β
β}) |
107 | 96, 106 | eleqtrrd 2835 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β π β (πΈβπ)) |
108 | 32, 37, 107, 87 | fvmptd3 6991 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))βπ) = sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ)), β*, <
)) |
109 | 24, 108 | eqtrd 2771 |
. . 3
β’ ((π β§ π β (β€β₯βπ)) β ((π»βπ)βπ) = sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ)), β*, <
)) |
110 | 1, 109 | mpteq2da 5223 |
. 2
β’ (π β (π β (β€β₯βπ) β¦ ((π»βπ)βπ)) = (π β (β€β₯βπ) β¦ sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)), β*, <
))) |
111 | 3 | eluzelz2 43791 |
. . . 4
β’ (π β π β π β β€) |
112 | 2, 111 | syl 17 |
. . 3
β’ (π β π β β€) |
113 | | eqid 2731 |
. . 3
β’
(β€β₯βπ) = (β€β₯βπ) |
114 | 75 | a1i 11 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) β V) |
115 | 75 | a1i 11 |
. . . . 5
β’ ((π β§ π β π) β ((πΉβπ)βπ) β V) |
116 | 46, 112, 73, 113, 3, 114, 115 | limsupequzmpt 44123 |
. . . 4
β’ (π β (lim supβ(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ))) = (lim supβ(π β π β¦ ((πΉβπ)βπ)))) |
117 | 116, 78 | eqeltrd 2832 |
. . 3
β’ (π β (lim supβ(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ))) β β) |
118 | 46, 112, 113, 69, 117 | supcnvlimsupmpt 44135 |
. 2
β’ (π β (π β (β€β₯βπ) β¦ sup(ran (π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)), β*, < )) β
(lim supβ(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)))) |
119 | 110, 118 | eqbrtrd 5147 |
1
β’ (π β (π β (β€β₯βπ) β¦ ((π»βπ)βπ)) β (lim supβ(π β
(β€β₯βπ) β¦ ((πΉβπ)βπ)))) |