Step | Hyp | Ref
| Expression |
1 | | nfcv 2903 |
. . 3
β’
β²ππΉ |
2 | | smfsuplem2.z |
. . 3
β’ π =
(β€β₯βπ) |
3 | | smfsuplem2.s |
. . 3
β’ (π β π β SAlg) |
4 | | smfsuplem2.f |
. . 3
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
5 | | eqid 2732 |
. . 3
β’
(topGenβran (,)) = (topGenβran (,)) |
6 | | eqid 2732 |
. . 3
β’
(SalGenβ(topGenβran (,))) = (SalGenβ(topGenβran
(,))) |
7 | | mnfxr 11273 |
. . . . 5
β’ -β
β β* |
8 | 7 | a1i 11 |
. . . 4
β’ (π β -β β
β*) |
9 | | smfsuplem2.8 |
. . . 4
β’ (π β π΄ β β) |
10 | 8, 9, 5, 6 | iocborel 45151 |
. . 3
β’ (π β (-β(,]π΄) β
(SalGenβ(topGenβran (,)))) |
11 | 1, 2, 3, 4, 5, 6, 10 | smfpimcc 45603 |
. 2
β’ (π β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) |
12 | | smfsuplem2.m |
. . . . . 6
β’ (π β π β β€) |
13 | 12 | adantr 481 |
. . . . 5
β’ ((π β§ (β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) β π β β€) |
14 | 3 | adantr 481 |
. . . . 5
β’ ((π β§ (β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) β π β SAlg) |
15 | 4 | adantr 481 |
. . . . 5
β’ ((π β§ (β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) β πΉ:πβΆ(SMblFnβπ)) |
16 | | smfsuplem2.d |
. . . . . 6
β’ π· = {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} |
17 | | fveq2 6891 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
18 | 17 | dmeqd 5905 |
. . . . . . . . 9
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
19 | 18 | cbviinv 5044 |
. . . . . . . 8
β’ β© π β π dom (πΉβπ) = β© π β π dom (πΉβπ) |
20 | 19 | a1i 11 |
. . . . . . 7
β’ (π₯ = π€ β β©
π β π dom (πΉβπ) = β© π β π dom (πΉβπ)) |
21 | | fveq2 6891 |
. . . . . . . . . . 11
β’ (π₯ = π€ β ((πΉβπ)βπ₯) = ((πΉβπ)βπ€)) |
22 | 21 | breq1d 5158 |
. . . . . . . . . 10
β’ (π₯ = π€ β (((πΉβπ)βπ₯) β€ π¦ β ((πΉβπ)βπ€) β€ π¦)) |
23 | 22 | ralbidv 3177 |
. . . . . . . . 9
β’ (π₯ = π€ β (βπ β π ((πΉβπ)βπ₯) β€ π¦ β βπ β π ((πΉβπ)βπ€) β€ π¦)) |
24 | 17 | fveq1d 6893 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβπ)βπ€) = ((πΉβπ)βπ€)) |
25 | 24 | breq1d 5158 |
. . . . . . . . . . 11
β’ (π = π β (((πΉβπ)βπ€) β€ π¦ β ((πΉβπ)βπ€) β€ π¦)) |
26 | 25 | cbvralvw 3234 |
. . . . . . . . . 10
β’
(βπ β
π ((πΉβπ)βπ€) β€ π¦ β βπ β π ((πΉβπ)βπ€) β€ π¦) |
27 | 26 | a1i 11 |
. . . . . . . . 9
β’ (π₯ = π€ β (βπ β π ((πΉβπ)βπ€) β€ π¦ β βπ β π ((πΉβπ)βπ€) β€ π¦)) |
28 | 23, 27 | bitrd 278 |
. . . . . . . 8
β’ (π₯ = π€ β (βπ β π ((πΉβπ)βπ₯) β€ π¦ β βπ β π ((πΉβπ)βπ€) β€ π¦)) |
29 | 28 | rexbidv 3178 |
. . . . . . 7
β’ (π₯ = π€ β (βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦ β βπ¦ β β βπ β π ((πΉβπ)βπ€) β€ π¦)) |
30 | 20, 29 | cbvrabv2w 43899 |
. . . . . 6
β’ {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} = {π€ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ€) β€ π¦} |
31 | 16, 30 | eqtri 2760 |
. . . . 5
β’ π· = {π€ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ€) β€ π¦} |
32 | | smfsuplem2.g |
. . . . . 6
β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) |
33 | 21 | mpteq2dv 5250 |
. . . . . . . . . 10
β’ (π₯ = π€ β (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ€))) |
34 | 24 | cbvmptv 5261 |
. . . . . . . . . . 11
β’ (π β π β¦ ((πΉβπ)βπ€)) = (π β π β¦ ((πΉβπ)βπ€)) |
35 | 34 | a1i 11 |
. . . . . . . . . 10
β’ (π₯ = π€ β (π β π β¦ ((πΉβπ)βπ€)) = (π β π β¦ ((πΉβπ)βπ€))) |
36 | 33, 35 | eqtrd 2772 |
. . . . . . . . 9
β’ (π₯ = π€ β (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ€))) |
37 | 36 | rneqd 5937 |
. . . . . . . 8
β’ (π₯ = π€ β ran (π β π β¦ ((πΉβπ)βπ₯)) = ran (π β π β¦ ((πΉβπ)βπ€))) |
38 | 37 | supeq1d 9443 |
. . . . . . 7
β’ (π₯ = π€ β sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < ) = sup(ran (π β π β¦ ((πΉβπ)βπ€)), β, < )) |
39 | 38 | cbvmptv 5261 |
. . . . . 6
β’ (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) = (π€ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ€)), β, < )) |
40 | 32, 39 | eqtri 2760 |
. . . . 5
β’ πΊ = (π€ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ€)), β, < )) |
41 | 9 | adantr 481 |
. . . . 5
β’ ((π β§ (β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) β π΄ β β) |
42 | | simprl 769 |
. . . . 5
β’ ((π β§ (β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) β β:πβΆπ) |
43 | | simplrr 776 |
. . . . . 6
β’ (((π β§ (β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) β§ π β π) β βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ))) |
44 | 17 | cnveqd 5875 |
. . . . . . . . 9
β’ (π = π β β‘(πΉβπ) = β‘(πΉβπ)) |
45 | 44 | imaeq1d 6058 |
. . . . . . . 8
β’ (π = π β (β‘(πΉβπ) β (-β(,]π΄)) = (β‘(πΉβπ) β (-β(,]π΄))) |
46 | | fveq2 6891 |
. . . . . . . . 9
β’ (π = π β (ββπ) = (ββπ)) |
47 | 46, 18 | ineq12d 4213 |
. . . . . . . 8
β’ (π = π β ((ββπ) β© dom (πΉβπ)) = ((ββπ) β© dom (πΉβπ))) |
48 | 45, 47 | eqeq12d 2748 |
. . . . . . 7
β’ (π = π β ((β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)) β (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) |
49 | 48 | rspccva 3611 |
. . . . . 6
β’
((βπ β
π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)) β§ π β π) β (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ))) |
50 | 43, 49 | sylancom 588 |
. . . . 5
β’ (((π β§ (β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) β§ π β π) β (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ))) |
51 | 13, 2, 14, 15, 31, 40, 41, 42, 50 | smfsuplem1 45606 |
. . . 4
β’ ((π β§ (β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ)))) β (β‘πΊ β (-β(,]π΄)) β (π βΎt π·)) |
52 | 51 | ex 413 |
. . 3
β’ (π β ((β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ))) β (β‘πΊ β (-β(,]π΄)) β (π βΎt π·))) |
53 | 52 | exlimdv 1936 |
. 2
β’ (π β (ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β (-β(,]π΄)) = ((ββπ) β© dom (πΉβπ))) β (β‘πΊ β (-β(,]π΄)) β (π βΎt π·))) |
54 | 11, 53 | mpd 15 |
1
β’ (π β (β‘πΊ β (-β(,]π΄)) β (π βΎt π·)) |