Step | Hyp | Ref
| Expression |
1 | | nfv 1917 |
. 2
β’
β²ππ |
2 | | smfsuplem3.s |
. 2
β’ (π β π β SAlg) |
3 | | smfsuplem3.d |
. . . . 5
β’ π· = {π₯ β β©
π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} |
4 | | ssrab2 4057 |
. . . . 5
β’ {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} β β©
π β π dom (πΉβπ) |
5 | 3, 4 | eqsstri 3996 |
. . . 4
β’ π· β β© π β π dom (πΉβπ) |
6 | 5 | a1i 11 |
. . 3
β’ (π β π· β β©
π β π dom (πΉβπ)) |
7 | | smfsuplem3.m |
. . . . . 6
β’ (π β π β β€) |
8 | | uzid 12802 |
. . . . . 6
β’ (π β β€ β π β
(β€β₯βπ)) |
9 | 7, 8 | syl 17 |
. . . . 5
β’ (π β π β (β€β₯βπ)) |
10 | | smfsuplem3.z |
. . . . 5
β’ π =
(β€β₯βπ) |
11 | 9, 10 | eleqtrrdi 2843 |
. . . 4
β’ (π β π β π) |
12 | | fveq2 6862 |
. . . . 5
β’ (π = π β (πΉβπ) = (πΉβπ)) |
13 | 12 | dmeqd 5881 |
. . . 4
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
14 | | smfsuplem3.f |
. . . . . 6
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
15 | 14, 11 | ffvelcdmd 7056 |
. . . . 5
β’ (π β (πΉβπ) β (SMblFnβπ)) |
16 | | eqid 2731 |
. . . . 5
β’ dom
(πΉβπ) = dom (πΉβπ) |
17 | 2, 15, 16 | smfdmss 45127 |
. . . 4
β’ (π β dom (πΉβπ) β βͺ π) |
18 | 11, 13, 17 | iinssd 43496 |
. . 3
β’ (π β β© π β π dom (πΉβπ) β βͺ π) |
19 | 6, 18 | sstrd 3972 |
. 2
β’ (π β π· β βͺ π) |
20 | | nfv 1917 |
. . . 4
β’
β²π(π β§ π₯ β π·) |
21 | 11 | ne0d 4315 |
. . . . 5
β’ (π β π β β
) |
22 | 21 | adantr 481 |
. . . 4
β’ ((π β§ π₯ β π·) β π β β
) |
23 | 2 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β π) β π β SAlg) |
24 | 14 | ffvelcdmda 7055 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
25 | | eqid 2731 |
. . . . . . 7
β’ dom
(πΉβπ) = dom (πΉβπ) |
26 | 23, 24, 25 | smff 45126 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
27 | 26 | adantlr 713 |
. . . . 5
β’ (((π β§ π₯ β π·) β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ) |
28 | | iinss2 5037 |
. . . . . . . 8
β’ (π β π β β©
π β π dom (πΉβπ) β dom (πΉβπ)) |
29 | 28 | adantl 482 |
. . . . . . 7
β’ ((π₯ β π· β§ π β π) β β©
π β π dom (πΉβπ) β dom (πΉβπ)) |
30 | 5 | sseli 3958 |
. . . . . . . 8
β’ (π₯ β π· β π₯ β β©
π β π dom (πΉβπ)) |
31 | 30 | adantr 481 |
. . . . . . 7
β’ ((π₯ β π· β§ π β π) β π₯ β β©
π β π dom (πΉβπ)) |
32 | 29, 31 | sseldd 3963 |
. . . . . 6
β’ ((π₯ β π· β§ π β π) β π₯ β dom (πΉβπ)) |
33 | 32 | adantll 712 |
. . . . 5
β’ (((π β§ π₯ β π·) β§ π β π) β π₯ β dom (πΉβπ)) |
34 | 27, 33 | ffvelcdmd 7056 |
. . . 4
β’ (((π β§ π₯ β π·) β§ π β π) β ((πΉβπ)βπ₯) β β) |
35 | 3 | reqabi 3440 |
. . . . . 6
β’ (π₯ β π· β (π₯ β β©
π β π dom (πΉβπ) β§ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦)) |
36 | 35 | simprbi 497 |
. . . . 5
β’ (π₯ β π· β βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦) |
37 | 36 | adantl 482 |
. . . 4
β’ ((π β§ π₯ β π·) β βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦) |
38 | 20, 22, 34, 37 | suprclrnmpt 43633 |
. . 3
β’ ((π β§ π₯ β π·) β sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < ) β
β) |
39 | | smfsuplem3.g |
. . 3
β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) |
40 | 38, 39 | fmptd 7082 |
. 2
β’ (π β πΊ:π·βΆβ) |
41 | 7 | adantr 481 |
. . 3
β’ ((π β§ π β β) β π β β€) |
42 | 2 | adantr 481 |
. . 3
β’ ((π β§ π β β) β π β SAlg) |
43 | 14 | adantr 481 |
. . 3
β’ ((π β§ π β β) β πΉ:πβΆ(SMblFnβπ)) |
44 | | simpr 485 |
. . 3
β’ ((π β§ π β β) β π β β) |
45 | 41, 10, 42, 43, 3, 39, 44 | smfsuplem2 45206 |
. 2
β’ ((π β§ π β β) β (β‘πΊ β (-β(,]π)) β (π βΎt π·)) |
46 | 1, 2, 19, 40, 45 | issmfle2d 45203 |
1
β’ (π β πΊ β (SMblFnβπ)) |