Step | Hyp | Ref
| Expression |
1 | | limsuplt2.1 |
. . 3
β’ (π β π΅ β β) |
2 | | limsuplt2.2 |
. . 3
β’ (π β πΉ:π΅βΆβ*) |
3 | | limsuplt2.3 |
. . 3
β’ (π β π΄ β
β*) |
4 | | eqid 2733 |
. . . 4
β’ (π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
5 | 4 | limsuplt 15367 |
. . 3
β’ ((π΅ β β β§ πΉ:π΅βΆβ* β§ π΄ β β*)
β ((lim supβπΉ)
< π΄ β βπ β β ((π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < ))βπ) < π΄)) |
6 | 1, 2, 3, 5 | syl3anc 1372 |
. 2
β’ (π β ((lim supβπΉ) < π΄ β βπ β β ((π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))βπ) < π΄)) |
7 | | oveq1 7365 |
. . . . . . . 8
β’ (π = π β (π[,)+β) = (π[,)+β)) |
8 | 7 | imaeq2d 6014 |
. . . . . . 7
β’ (π = π β (πΉ β (π[,)+β)) = (πΉ β (π[,)+β))) |
9 | 8 | ineq1d 4172 |
. . . . . 6
β’ (π = π β ((πΉ β (π[,)+β)) β© β*) =
((πΉ β (π[,)+β)) β©
β*)) |
10 | 9 | supeq1d 9387 |
. . . . 5
β’ (π = π β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
11 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
12 | | xrltso 13066 |
. . . . . . 7
β’ < Or
β* |
13 | 12 | supex 9404 |
. . . . . 6
β’
sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β V |
14 | 13 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β V) |
15 | 4, 10, 11, 14 | fvmptd3 6972 |
. . . 4
β’ ((π β§ π β β) β ((π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))βπ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
16 | 15 | breq1d 5116 |
. . 3
β’ ((π β§ π β β) β (((π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))βπ) < π΄ β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) < π΄)) |
17 | 16 | rexbidva 3170 |
. 2
β’ (π β (βπ β β ((π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))βπ) < π΄ β βπ β β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) < π΄)) |
18 | | oveq1 7365 |
. . . . . . . 8
β’ (π = π β (π[,)+β) = (π[,)+β)) |
19 | 18 | imaeq2d 6014 |
. . . . . . 7
β’ (π = π β (πΉ β (π[,)+β)) = (πΉ β (π[,)+β))) |
20 | 19 | ineq1d 4172 |
. . . . . 6
β’ (π = π β ((πΉ β (π[,)+β)) β© β*) =
((πΉ β (π[,)+β)) β©
β*)) |
21 | 20 | supeq1d 9387 |
. . . . 5
β’ (π = π β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
22 | 21 | breq1d 5116 |
. . . 4
β’ (π = π β (sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) < π΄ β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) < π΄)) |
23 | 22 | cbvrexvw 3225 |
. . 3
β’
(βπ β
β sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) < π΄ β βπ β β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) < π΄) |
24 | 23 | a1i 11 |
. 2
β’ (π β (βπ β β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) < π΄ β βπ β β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) < π΄)) |
25 | 6, 17, 24 | 3bitrd 305 |
1
β’ (π β ((lim supβπΉ) < π΄ β βπ β β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) < π΄)) |