Step | Hyp | Ref
| Expression |
1 | | nfmpt1 5257 |
. . 3
β’
β²π(π β π β¦ π΅) |
2 | | limsupreuzmpt.m |
. . 3
β’ (π β π β β€) |
3 | | limsupreuzmpt.z |
. . 3
β’ π =
(β€β₯βπ) |
4 | | limsupreuzmpt.j |
. . . 4
β’
β²ππ |
5 | | limsupreuzmpt.b |
. . . 4
β’ ((π β§ π β π) β π΅ β β) |
6 | 4, 5 | fmptd2f 43937 |
. . 3
β’ (π β (π β π β¦ π΅):πβΆβ) |
7 | 1, 2, 3, 6 | limsupreuz 44453 |
. 2
β’ (π β ((lim supβ(π β π β¦ π΅)) β β β (βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ ((π β π β¦ π΅)βπ) β§ βπ¦ β β βπ β π ((π β π β¦ π΅)βπ) β€ π¦))) |
8 | | nfv 1918 |
. . . . . . . 8
β’
β²π π β π |
9 | 4, 8 | nfan 1903 |
. . . . . . 7
β’
β²π(π β§ π β π) |
10 | | simpll 766 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
11 | 3 | uztrn2 12841 |
. . . . . . . . . 10
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
12 | 11 | adantll 713 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
13 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β π β¦ π΅) = (π β π β¦ π΅) |
14 | 13 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π β π β¦ π΅) = (π β π β¦ π΅)) |
15 | 14, 5 | fvmpt2d 7012 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = π΅) |
16 | 10, 12, 15 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((π β π β¦ π΅)βπ) = π΅) |
17 | 16 | breq2d 5161 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (π¦ β€ ((π β π β¦ π΅)βπ) β π¦ β€ π΅)) |
18 | 9, 17 | rexbida 3270 |
. . . . . 6
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)π¦ β€ ((π β π β¦ π΅)βπ) β βπ β (β€β₯βπ)π¦ β€ π΅)) |
19 | 18 | ralbidva 3176 |
. . . . 5
β’ (π β (βπ β π βπ β (β€β₯βπ)π¦ β€ ((π β π β¦ π΅)βπ) β βπ β π βπ β (β€β₯βπ)π¦ β€ π΅)) |
20 | 19 | rexbidv 3179 |
. . . 4
β’ (π β (βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ ((π β π β¦ π΅)βπ) β βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ π΅)) |
21 | | breq1 5152 |
. . . . . . . . 9
β’ (π¦ = π₯ β (π¦ β€ π΅ β π₯ β€ π΅)) |
22 | 21 | rexbidv 3179 |
. . . . . . . 8
β’ (π¦ = π₯ β (βπ β (β€β₯βπ)π¦ β€ π΅ β βπ β (β€β₯βπ)π₯ β€ π΅)) |
23 | 22 | ralbidv 3178 |
. . . . . . 7
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)π¦ β€ π΅ β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅)) |
24 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
25 | 24 | rexeqdv 3327 |
. . . . . . . . 9
β’ (π = π β (βπ β (β€β₯βπ)π₯ β€ π΅ β βπ β (β€β₯βπ)π₯ β€ π΅)) |
26 | 25 | cbvralvw 3235 |
. . . . . . . 8
β’
(βπ β
π βπ β (β€β₯βπ)π₯ β€ π΅ β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅) |
27 | 26 | a1i 11 |
. . . . . . 7
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)π₯ β€ π΅ β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅)) |
28 | 23, 27 | bitrd 279 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)π¦ β€ π΅ β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅)) |
29 | 28 | cbvrexvw 3236 |
. . . . 5
β’
(βπ¦ β
β βπ β
π βπ β (β€β₯βπ)π¦ β€ π΅ β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅) |
30 | 29 | a1i 11 |
. . . 4
β’ (π β (βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ π΅ β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅)) |
31 | 20, 30 | bitrd 279 |
. . 3
β’ (π β (βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ ((π β π β¦ π΅)βπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅)) |
32 | 15 | breq1d 5159 |
. . . . . 6
β’ ((π β§ π β π) β (((π β π β¦ π΅)βπ) β€ π¦ β π΅ β€ π¦)) |
33 | 4, 32 | ralbida 3268 |
. . . . 5
β’ (π β (βπ β π ((π β π β¦ π΅)βπ) β€ π¦ β βπ β π π΅ β€ π¦)) |
34 | 33 | rexbidv 3179 |
. . . 4
β’ (π β (βπ¦ β β βπ β π ((π β π β¦ π΅)βπ) β€ π¦ β βπ¦ β β βπ β π π΅ β€ π¦)) |
35 | | breq2 5153 |
. . . . . . 7
β’ (π¦ = π₯ β (π΅ β€ π¦ β π΅ β€ π₯)) |
36 | 35 | ralbidv 3178 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π π΅ β€ π¦ β βπ β π π΅ β€ π₯)) |
37 | 36 | cbvrexvw 3236 |
. . . . 5
β’
(βπ¦ β
β βπ β
π π΅ β€ π¦ β βπ₯ β β βπ β π π΅ β€ π₯) |
38 | 37 | a1i 11 |
. . . 4
β’ (π β (βπ¦ β β βπ β π π΅ β€ π¦ β βπ₯ β β βπ β π π΅ β€ π₯)) |
39 | 34, 38 | bitrd 279 |
. . 3
β’ (π β (βπ¦ β β βπ β π ((π β π β¦ π΅)βπ) β€ π¦ β βπ₯ β β βπ β π π΅ β€ π₯)) |
40 | 31, 39 | anbi12d 632 |
. 2
β’ (π β ((βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ ((π β π β¦ π΅)βπ) β§ βπ¦ β β βπ β π ((π β π β¦ π΅)βπ) β€ π¦) β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅ β§ βπ₯ β β βπ β π π΅ β€ π₯))) |
41 | 7, 40 | bitrd 279 |
1
β’ (π β ((lim supβ(π β π β¦ π΅)) β β β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅ β§ βπ₯ β β βπ β π π΅ β€ π₯))) |