Step | Hyp | Ref
| Expression |
1 | | smfliminf.m |
. 2
β’ (π β π β β€) |
2 | | smfliminf.z |
. 2
β’ π =
(β€β₯βπ) |
3 | | smfliminf.s |
. 2
β’ (π β π β SAlg) |
4 | | smfliminf.f |
. 2
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
5 | | smfliminf.d |
. . 3
β’ π· = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} |
6 | | nfcv 2904 |
. . . . 5
β’
β²πβ© π β
(β€β₯βπ)dom (πΉβπ) |
7 | | nfcv 2904 |
. . . . 5
β’
β²πβ© π β
(β€β₯βπ)dom (πΉβπ) |
8 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
9 | 8 | iineq1d 43388 |
. . . . . 6
β’ (π = π β β©
π β
(β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ)) |
10 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π(πΉβπ) |
11 | 10 | nfdm 5907 |
. . . . . . . 8
β’
β²πdom
(πΉβπ) |
12 | | smfliminf.n |
. . . . . . . . . 10
β’
β²ππΉ |
13 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²ππ |
14 | 12, 13 | nffv 6853 |
. . . . . . . . 9
β’
β²π(πΉβπ) |
15 | 14 | nfdm 5907 |
. . . . . . . 8
β’
β²πdom
(πΉβπ) |
16 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
17 | 16 | dmeqd 5862 |
. . . . . . . 8
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
18 | 11, 15, 17 | cbviin 4998 |
. . . . . . 7
β’ β© π β (β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ) |
19 | 18 | a1i 11 |
. . . . . 6
β’ (π = π β β©
π β
(β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ)) |
20 | 9, 19 | eqtrd 2773 |
. . . . 5
β’ (π = π β β©
π β
(β€β₯βπ)dom (πΉβπ) = β© π β
(β€β₯βπ)dom (πΉβπ)) |
21 | 6, 7, 20 | cbviun 4997 |
. . . 4
β’ βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) = βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
22 | 21 | rabeqi 3419 |
. . 3
β’ {π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} = {π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} |
23 | | nfcv 2904 |
. . . . 5
β’
β²π₯π |
24 | | nfcv 2904 |
. . . . . 6
β’
β²π₯(β€β₯βπ) |
25 | | smfliminf.x |
. . . . . . . 8
β’
β²π₯πΉ |
26 | | nfcv 2904 |
. . . . . . . 8
β’
β²π₯π |
27 | 25, 26 | nffv 6853 |
. . . . . . 7
β’
β²π₯(πΉβπ) |
28 | 27 | nfdm 5907 |
. . . . . 6
β’
β²π₯dom
(πΉβπ) |
29 | 24, 28 | nfiin 4986 |
. . . . 5
β’
β²π₯β© π β
(β€β₯βπ)dom (πΉβπ) |
30 | 23, 29 | nfiun 4985 |
. . . 4
β’
β²π₯βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
31 | | nfcv 2904 |
. . . 4
β’
β²π¦βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) |
32 | | nfv 1918 |
. . . 4
β’
β²π¦(lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) β β |
33 | | nfcv 2904 |
. . . . . 6
β’
β²π₯lim
inf |
34 | | nfcv 2904 |
. . . . . . . 8
β’
β²π₯π¦ |
35 | 27, 34 | nffv 6853 |
. . . . . . 7
β’
β²π₯((πΉβπ)βπ¦) |
36 | 23, 35 | nfmpt 5213 |
. . . . . 6
β’
β²π₯(π β π β¦ ((πΉβπ)βπ¦)) |
37 | 33, 36 | nffv 6853 |
. . . . 5
β’
β²π₯(lim
infβ(π β π β¦ ((πΉβπ)βπ¦))) |
38 | | nfcv 2904 |
. . . . 5
β’
β²π₯β |
39 | 37, 38 | nfel 2918 |
. . . 4
β’
β²π₯(lim
infβ(π β π β¦ ((πΉβπ)βπ¦))) β β |
40 | | nfv 1918 |
. . . . . . . 8
β’
β²π π₯ = π¦ |
41 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((πΉβπ)βπ₯) = ((πΉβπ)βπ¦)) |
42 | 41 | adantr 482 |
. . . . . . . 8
β’ ((π₯ = π¦ β§ π β π) β ((πΉβπ)βπ₯) = ((πΉβπ)βπ¦)) |
43 | 40, 42 | mpteq2da 5204 |
. . . . . . 7
β’ (π₯ = π¦ β (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ¦))) |
44 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π((πΉβπ)βπ¦) |
45 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²ππ¦ |
46 | 14, 45 | nffv 6853 |
. . . . . . . . 9
β’
β²π((πΉβπ)βπ¦) |
47 | 16 | fveq1d 6845 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ)βπ¦) = ((πΉβπ)βπ¦)) |
48 | 44, 46, 47 | cbvmpt 5217 |
. . . . . . . 8
β’ (π β π β¦ ((πΉβπ)βπ¦)) = (π β π β¦ ((πΉβπ)βπ¦)) |
49 | 48 | a1i 11 |
. . . . . . 7
β’ (π₯ = π¦ β (π β π β¦ ((πΉβπ)βπ¦)) = (π β π β¦ ((πΉβπ)βπ¦))) |
50 | 43, 49 | eqtrd 2773 |
. . . . . 6
β’ (π₯ = π¦ β (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ¦))) |
51 | 50 | fveq2d 6847 |
. . . . 5
β’ (π₯ = π¦ β (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) = (lim infβ(π β π β¦ ((πΉβπ)βπ¦)))) |
52 | 51 | eleq1d 2819 |
. . . 4
β’ (π₯ = π¦ β ((lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β β (lim
infβ(π β π β¦ ((πΉβπ)βπ¦))) β β)) |
53 | 30, 31, 32, 39, 52 | cbvrabw 3438 |
. . 3
β’ {π₯ β βͺ π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} = {π¦ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ¦))) β β} |
54 | 5, 22, 53 | 3eqtri 2765 |
. 2
β’ π· = {π¦ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ¦))) β β} |
55 | | smfliminf.g |
. . 3
β’ πΊ = (π₯ β π· β¦ (lim infβ(π β π β¦ ((πΉβπ)βπ₯)))) |
56 | | nfrab1 3425 |
. . . . 5
β’
β²π₯{π₯ β βͺ
π β π β© π β
(β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} |
57 | 5, 56 | nfcxfr 2902 |
. . . 4
β’
β²π₯π· |
58 | | nfcv 2904 |
. . . 4
β’
β²π¦π· |
59 | | nfcv 2904 |
. . . 4
β’
β²π¦(lim
infβ(π β π β¦ ((πΉβπ)βπ₯))) |
60 | 57, 58, 59, 37, 51 | cbvmptf 5215 |
. . 3
β’ (π₯ β π· β¦ (lim infβ(π β π β¦ ((πΉβπ)βπ₯)))) = (π¦ β π· β¦ (lim infβ(π β π β¦ ((πΉβπ)βπ¦)))) |
61 | 55, 60 | eqtri 2761 |
. 2
β’ πΊ = (π¦ β π· β¦ (lim infβ(π β π β¦ ((πΉβπ)βπ¦)))) |
62 | 1, 2, 3, 4, 54, 61 | smfliminflem 45157 |
1
β’ (π β πΊ β (SMblFnβπ)) |