Step | Hyp | Ref
| Expression |
1 | | resimass 43928 |
. . . . . . . . 9
β’ ((πΉ βΎ π΄) β (π[,)+β)) β (πΉ β (π[,)+β)) |
2 | 1 | a1i 11 |
. . . . . . . 8
β’ (π β ((πΉ βΎ π΄) β (π[,)+β)) β (πΉ β (π[,)+β))) |
3 | 2 | ssrind 4234 |
. . . . . . 7
β’ (π β (((πΉ βΎ π΄) β (π[,)+β)) β© β*)
β ((πΉ β (π[,)+β)) β©
β*)) |
4 | | liminfresxr.2 |
. . . . . . . . . . . . 13
β’ (π β Fun πΉ) |
5 | 4 | funfnd 6576 |
. . . . . . . . . . . 12
β’ (π β πΉ Fn dom πΉ) |
6 | | elinel1 4194 |
. . . . . . . . . . . 12
β’ (π¦ β ((πΉ β (π[,)+β)) β© β*)
β π¦ β (πΉ β (π[,)+β))) |
7 | | fvelima2 43950 |
. . . . . . . . . . . 12
β’ ((πΉ Fn dom πΉ β§ π¦ β (πΉ β (π[,)+β))) β βπ₯ β (dom πΉ β© (π[,)+β))(πΉβπ₯) = π¦) |
8 | 5, 6, 7 | syl2an 596 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β βπ₯ β (dom
πΉ β© (π[,)+β))(πΉβπ₯) = π¦) |
9 | | elinel1 4194 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β (dom πΉ β© (π[,)+β)) β π₯ β dom πΉ) |
10 | 9 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ β ((πΉ β (π[,)+β)) β© β*)
β§ π₯ β (dom πΉ β© (π[,)+β)) β§ (πΉβπ₯) = π¦) β π₯ β dom πΉ) |
11 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β ((πΉ β (π[,)+β)) β© β*)
β§ (πΉβπ₯) = π¦) β (πΉβπ₯) = π¦) |
12 | | elinel2 4195 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β ((πΉ β (π[,)+β)) β© β*)
β π¦ β
β*) |
13 | 12 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β ((πΉ β (π[,)+β)) β© β*)
β§ (πΉβπ₯) = π¦) β π¦ β β*) |
14 | 11, 13 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ β ((πΉ β (π[,)+β)) β© β*)
β§ (πΉβπ₯) = π¦) β (πΉβπ₯) β
β*) |
15 | 14 | 3adant2 1131 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ β ((πΉ β (π[,)+β)) β© β*)
β§ π₯ β (dom πΉ β© (π[,)+β)) β§ (πΉβπ₯) = π¦) β (πΉβπ₯) β
β*) |
16 | 10, 15 | jca 512 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β ((πΉ β (π[,)+β)) β© β*)
β§ π₯ β (dom πΉ β© (π[,)+β)) β§ (πΉβπ₯) = π¦) β (π₯ β dom πΉ β§ (πΉβπ₯) β
β*)) |
17 | 16 | 3adant1l 1176 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β)) β§ (πΉβπ₯) = π¦) β (π₯ β dom πΉ β§ (πΉβπ₯) β
β*)) |
18 | | simp1l 1197 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β)) β§ (πΉβπ₯) = π¦) β π) |
19 | | elpreima 7056 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΉ Fn dom πΉ β (π₯ β (β‘πΉ β β*) β (π₯ β dom πΉ β§ (πΉβπ₯) β
β*))) |
20 | 5, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π₯ β (β‘πΉ β β*) β (π₯ β dom πΉ β§ (πΉβπ₯) β
β*))) |
21 | 18, 20 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β)) β§ (πΉβπ₯) = π¦) β (π₯ β (β‘πΉ β β*) β (π₯ β dom πΉ β§ (πΉβπ₯) β
β*))) |
22 | 17, 21 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β)) β§ (πΉβπ₯) = π¦) β π₯ β (β‘πΉ β
β*)) |
23 | | liminfresxr.3 |
. . . . . . . . . . . . . . . . 17
β’ π΄ = (β‘πΉ β
β*) |
24 | 22, 23 | eleqtrrdi 2844 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β)) β§ (πΉβπ₯) = π¦) β π₯ β π΄) |
25 | 24 | 3expa 1118 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β π₯ β π΄) |
26 | 25 | fvresd 6908 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β ((πΉ βΎ π΄)βπ₯) = (πΉβπ₯)) |
27 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β (πΉβπ₯) = π¦) |
28 | 26, 27 | eqtr2d 2773 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β π¦ = ((πΉ βΎ π΄)βπ₯)) |
29 | | simplll 773 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β π) |
30 | 4 | funresd 6588 |
. . . . . . . . . . . . . . . 16
β’ (π β Fun (πΉ βΎ π΄)) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β Fun (πΉ βΎ π΄)) |
32 | 9 | ad2antlr 725 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β π₯ β dom πΉ) |
33 | 25, 32 | elind 4193 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β π₯ β (π΄ β© dom πΉ)) |
34 | | dmres 6001 |
. . . . . . . . . . . . . . . 16
β’ dom
(πΉ βΎ π΄) = (π΄ β© dom πΉ) |
35 | 33, 34 | eleqtrrdi 2844 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β π₯ β dom (πΉ βΎ π΄)) |
36 | 31, 35 | jca 512 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β (Fun (πΉ βΎ π΄) β§ π₯ β dom (πΉ βΎ π΄))) |
37 | | elinel2 4195 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (dom πΉ β© (π[,)+β)) β π₯ β (π[,)+β)) |
38 | 37 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β π₯ β (π[,)+β)) |
39 | | funfvima 7228 |
. . . . . . . . . . . . . 14
β’ ((Fun
(πΉ βΎ π΄) β§ π₯ β dom (πΉ βΎ π΄)) β (π₯ β (π[,)+β) β ((πΉ βΎ π΄)βπ₯) β ((πΉ βΎ π΄) β (π[,)+β)))) |
40 | 36, 38, 39 | sylc 65 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β ((πΉ βΎ π΄)βπ₯) β ((πΉ βΎ π΄) β (π[,)+β))) |
41 | 28, 40 | eqeltrd 2833 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β§ π₯ β (dom πΉ β© (π[,)+β))) β§ (πΉβπ₯) = π¦) β π¦ β ((πΉ βΎ π΄) β (π[,)+β))) |
42 | 41 | rexlimdva2 3157 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β (βπ₯ β
(dom πΉ β© (π[,)+β))(πΉβπ₯) = π¦ β π¦ β ((πΉ βΎ π΄) β (π[,)+β)))) |
43 | 8, 42 | mpd 15 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((πΉ β (π[,)+β)) β© β*))
β π¦ β ((πΉ βΎ π΄) β (π[,)+β))) |
44 | 43 | ralrimiva 3146 |
. . . . . . . . 9
β’ (π β βπ¦ β ((πΉ β (π[,)+β)) β© β*)π¦ β ((πΉ βΎ π΄) β (π[,)+β))) |
45 | | dfss3 3969 |
. . . . . . . . 9
β’ (((πΉ β (π[,)+β)) β© β*)
β ((πΉ βΎ π΄) β (π[,)+β)) β βπ¦ β ((πΉ β (π[,)+β)) β© β*)π¦ β ((πΉ βΎ π΄) β (π[,)+β))) |
46 | 44, 45 | sylibr 233 |
. . . . . . . 8
β’ (π β ((πΉ β (π[,)+β)) β© β*)
β ((πΉ βΎ π΄) β (π[,)+β))) |
47 | | inss2 4228 |
. . . . . . . . 9
β’ ((πΉ β (π[,)+β)) β© β*)
β β* |
48 | 47 | a1i 11 |
. . . . . . . 8
β’ (π β ((πΉ β (π[,)+β)) β© β*)
β β*) |
49 | 46, 48 | ssind 4231 |
. . . . . . 7
β’ (π β ((πΉ β (π[,)+β)) β© β*)
β (((πΉ βΎ π΄) β (π[,)+β)) β©
β*)) |
50 | 3, 49 | eqssd 3998 |
. . . . . 6
β’ (π β (((πΉ βΎ π΄) β (π[,)+β)) β© β*) =
((πΉ β (π[,)+β)) β©
β*)) |
51 | 50 | infeq1d 9468 |
. . . . 5
β’ (π β inf((((πΉ βΎ π΄) β (π[,)+β)) β© β*),
β*, < ) = inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
52 | 51 | mpteq2dv 5249 |
. . . 4
β’ (π β (π β β β¦ inf((((πΉ βΎ π΄) β (π[,)+β)) β© β*),
β*, < )) = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
53 | 52 | rneqd 5935 |
. . 3
β’ (π β ran (π β β β¦ inf((((πΉ βΎ π΄) β (π[,)+β)) β© β*),
β*, < )) = ran (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
54 | 53 | supeq1d 9437 |
. 2
β’ (π β sup(ran (π β β β¦
inf((((πΉ βΎ π΄) β (π[,)+β)) β© β*),
β*, < )), β*, < ) = sup(ran (π β β β¦
inf(((πΉ β (π[,)+β)) β©
β*), β*, < )), β*, <
)) |
55 | | liminfresxr.1 |
. . . 4
β’ (π β πΉ β π) |
56 | 55 | resexd 6026 |
. . 3
β’ (π β (πΉ βΎ π΄) β V) |
57 | | eqid 2732 |
. . . 4
β’ (π β β β¦
inf((((πΉ βΎ π΄) β (π[,)+β)) β© β*),
β*, < )) = (π β β β¦ inf((((πΉ βΎ π΄) β (π[,)+β)) β© β*),
β*, < )) |
58 | 57 | liminfval 44461 |
. . 3
β’ ((πΉ βΎ π΄) β V β (lim infβ(πΉ βΎ π΄)) = sup(ran (π β β β¦ inf((((πΉ βΎ π΄) β (π[,)+β)) β© β*),
β*, < )), β*, < )) |
59 | 56, 58 | syl 17 |
. 2
β’ (π β (lim infβ(πΉ βΎ π΄)) = sup(ran (π β β β¦ inf((((πΉ βΎ π΄) β (π[,)+β)) β© β*),
β*, < )), β*, < )) |
60 | | eqid 2732 |
. . . 4
β’ (π β β β¦
inf(((πΉ β (π[,)+β)) β©
β*), β*, < )) = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
61 | 60 | liminfval 44461 |
. . 3
β’ (πΉ β π β (lim infβπΉ) = sup(ran (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )), β*, < )) |
62 | 55, 61 | syl 17 |
. 2
β’ (π β (lim infβπΉ) = sup(ran (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )), β*, < )) |
63 | 54, 59, 62 | 3eqtr4d 2782 |
1
β’ (π β (lim infβ(πΉ βΎ π΄)) = (lim infβπΉ)) |