Step | Hyp | Ref
| Expression |
1 | | limsupge.b |
. . . 4
β’ (π β π΅ β β) |
2 | | limsupge.f |
. . . 4
β’ (π β πΉ:π΅βΆβ*) |
3 | | limsupge.a |
. . . 4
β’ (π β π΄ β
β*) |
4 | | eqid 2733 |
. . . . 5
β’ (π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
5 | 4 | limsuple 15366 |
. . . 4
β’ ((π΅ β β β§ πΉ:π΅βΆβ* β§ π΄ β β*)
β (π΄ β€ (lim
supβπΉ) β
βπ β β
π΄ β€ ((π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))βπ))) |
6 | 1, 2, 3, 5 | syl3anc 1372 |
. . 3
β’ (π β (π΄ β€ (lim supβπΉ) β βπ β β π΄ β€ ((π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))βπ))) |
7 | | oveq1 7365 |
. . . . . . . . 9
β’ (π = π β (π[,)+β) = (π[,)+β)) |
8 | 7 | imaeq2d 6014 |
. . . . . . . 8
β’ (π = π β (πΉ β (π[,)+β)) = (πΉ β (π[,)+β))) |
9 | 8 | ineq1d 4172 |
. . . . . . 7
β’ (π = π β ((πΉ β (π[,)+β)) β© β*) =
((πΉ β (π[,)+β)) β©
β*)) |
10 | 9 | supeq1d 9387 |
. . . . . 6
β’ (π = π β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
11 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
12 | | xrltso 13066 |
. . . . . . . 8
β’ < Or
β* |
13 | 12 | supex 9404 |
. . . . . . 7
β’
sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β V |
14 | 13 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β V) |
15 | 4, 10, 11, 14 | fvmptd3 6972 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))βπ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
16 | 15 | breq2d 5118 |
. . . 4
β’ ((π β§ π β β) β (π΄ β€ ((π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))βπ) β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
17 | 16 | ralbidva 3169 |
. . 3
β’ (π β (βπ β β π΄ β€ ((π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))βπ) β βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
18 | 6, 17 | bitrd 279 |
. 2
β’ (π β (π΄ β€ (lim supβπΉ) β βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
19 | | oveq1 7365 |
. . . . . . . 8
β’ (π = π β (π[,)+β) = (π[,)+β)) |
20 | 19 | imaeq2d 6014 |
. . . . . . 7
β’ (π = π β (πΉ β (π[,)+β)) = (πΉ β (π[,)+β))) |
21 | 20 | ineq1d 4172 |
. . . . . 6
β’ (π = π β ((πΉ β (π[,)+β)) β© β*) =
((πΉ β (π[,)+β)) β©
β*)) |
22 | 21 | supeq1d 9387 |
. . . . 5
β’ (π = π β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
23 | 22 | breq2d 5118 |
. . . 4
β’ (π = π β (π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
24 | 23 | cbvralvw 3224 |
. . 3
β’
(βπ β
β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
25 | 24 | a1i 11 |
. 2
β’ (π β (βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
26 | 18, 25 | bitrd 279 |
1
β’ (π β (π΄ β€ (lim supβπΉ) β βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |