Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. 2
β’
β²ππ |
2 | | incsmf.j |
. . . . 5
β’ π½ = (topGenβran
(,)) |
3 | | retop 24141 |
. . . . 5
β’
(topGenβran (,)) β Top |
4 | 2, 3 | eqeltri 2830 |
. . . 4
β’ π½ β Top |
5 | 4 | a1i 11 |
. . 3
β’ (π β π½ β Top) |
6 | | incsmf.b |
. . 3
β’ π΅ = (SalGenβπ½) |
7 | 5, 6 | salgencld 44676 |
. 2
β’ (π β π΅ β SAlg) |
8 | | incsmf.a |
. . 3
β’ (π β π΄ β β) |
9 | 5, 6 | unisalgen2 44681 |
. . . 4
β’ (π β βͺ π΅ =
βͺ π½) |
10 | 2 | unieqi 4879 |
. . . . 5
β’ βͺ π½ =
βͺ (topGenβran (,)) |
11 | 10 | a1i 11 |
. . . 4
β’ (π β βͺ π½ =
βͺ (topGenβran (,))) |
12 | | uniretop 24142 |
. . . . . 6
β’ β =
βͺ (topGenβran (,)) |
13 | 12 | eqcomi 2742 |
. . . . 5
β’ βͺ (topGenβran (,)) = β |
14 | 13 | a1i 11 |
. . . 4
β’ (π β βͺ (topGenβran (,)) = β) |
15 | 9, 11, 14 | 3eqtrrd 2778 |
. . 3
β’ (π β β = βͺ π΅) |
16 | 8, 15 | sseqtrd 3985 |
. 2
β’ (π β π΄ β βͺ π΅) |
17 | | incsmf.f |
. 2
β’ (π β πΉ:π΄βΆβ) |
18 | | nfv 1918 |
. . . 4
β’
β²π€(π β§ π β β) |
19 | | nfv 1918 |
. . . 4
β’
β²π§(π β§ π β β) |
20 | 8 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β π΄ β β) |
21 | 17 | frexr 43706 |
. . . . 5
β’ (π β πΉ:π΄βΆβ*) |
22 | 21 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β πΉ:π΄βΆβ*) |
23 | | incsmf.i |
. . . . . 6
β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) |
24 | | breq1 5109 |
. . . . . . . 8
β’ (π₯ = π€ β (π₯ β€ π¦ β π€ β€ π¦)) |
25 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = π€ β (πΉβπ₯) = (πΉβπ€)) |
26 | 25 | breq1d 5116 |
. . . . . . . 8
β’ (π₯ = π€ β ((πΉβπ₯) β€ (πΉβπ¦) β (πΉβπ€) β€ (πΉβπ¦))) |
27 | 24, 26 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π€ β ((π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦)) β (π€ β€ π¦ β (πΉβπ€) β€ (πΉβπ¦)))) |
28 | | breq2 5110 |
. . . . . . . 8
β’ (π¦ = π§ β (π€ β€ π¦ β π€ β€ π§)) |
29 | | fveq2 6843 |
. . . . . . . . 9
β’ (π¦ = π§ β (πΉβπ¦) = (πΉβπ§)) |
30 | 29 | breq2d 5118 |
. . . . . . . 8
β’ (π¦ = π§ β ((πΉβπ€) β€ (πΉβπ¦) β (πΉβπ€) β€ (πΉβπ§))) |
31 | 28, 30 | imbi12d 345 |
. . . . . . 7
β’ (π¦ = π§ β ((π€ β€ π¦ β (πΉβπ€) β€ (πΉβπ¦)) β (π€ β€ π§ β (πΉβπ€) β€ (πΉβπ§)))) |
32 | 27, 31 | cbvral2vw 3226 |
. . . . . 6
β’
(βπ₯ β
π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦)) β βπ€ β π΄ βπ§ β π΄ (π€ β€ π§ β (πΉβπ€) β€ (πΉβπ§))) |
33 | 23, 32 | sylib 217 |
. . . . 5
β’ (π β βπ€ β π΄ βπ§ β π΄ (π€ β€ π§ β (πΉβπ€) β€ (πΉβπ§))) |
34 | 33 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β βπ€ β π΄ βπ§ β π΄ (π€ β€ π§ β (πΉβπ€) β€ (πΉβπ§))) |
35 | | rexr 11206 |
. . . . 5
β’ (π β β β π β
β*) |
36 | 35 | adantl 483 |
. . . 4
β’ ((π β§ π β β) β π β β*) |
37 | 25 | breq1d 5116 |
. . . . 5
β’ (π₯ = π€ β ((πΉβπ₯) < π β (πΉβπ€) < π)) |
38 | 37 | cbvrabv 3416 |
. . . 4
β’ {π₯ β π΄ β£ (πΉβπ₯) < π} = {π€ β π΄ β£ (πΉβπ€) < π} |
39 | | eqid 2733 |
. . . 4
β’
sup({π₯ β π΄ β£ (πΉβπ₯) < π}, β*, < ) = sup({π₯ β π΄ β£ (πΉβπ₯) < π}, β*, <
) |
40 | | eqid 2733 |
. . . 4
β’
(-β(,)sup({π₯
β π΄ β£ (πΉβπ₯) < π}, β*, < )) =
(-β(,)sup({π₯ β
π΄ β£ (πΉβπ₯) < π}, β*, <
)) |
41 | | eqid 2733 |
. . . 4
β’
(-β(,]sup({π₯
β π΄ β£ (πΉβπ₯) < π}, β*, < )) =
(-β(,]sup({π₯ β
π΄ β£ (πΉβπ₯) < π}, β*, <
)) |
42 | 18, 19, 20, 22, 34, 2, 6, 36, 38, 39, 40, 41 | incsmflem 45068 |
. . 3
β’ ((π β§ π β β) β βπ β π΅ {π₯ β π΄ β£ (πΉβπ₯) < π} = (π β© π΄)) |
43 | | reex 11147 |
. . . . . . 7
β’ β
β V |
44 | 43 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
45 | 44, 8 | ssexd 5282 |
. . . . 5
β’ (π β π΄ β V) |
46 | | elrest 17314 |
. . . . 5
β’ ((π΅ β SAlg β§ π΄ β V) β ({π₯ β π΄ β£ (πΉβπ₯) < π} β (π΅ βΎt π΄) β βπ β π΅ {π₯ β π΄ β£ (πΉβπ₯) < π} = (π β© π΄))) |
47 | 7, 45, 46 | syl2anc 585 |
. . . 4
β’ (π β ({π₯ β π΄ β£ (πΉβπ₯) < π} β (π΅ βΎt π΄) β βπ β π΅ {π₯ β π΄ β£ (πΉβπ₯) < π} = (π β© π΄))) |
48 | 47 | adantr 482 |
. . 3
β’ ((π β§ π β β) β ({π₯ β π΄ β£ (πΉβπ₯) < π} β (π΅ βΎt π΄) β βπ β π΅ {π₯ β π΄ β£ (πΉβπ₯) < π} = (π β© π΄))) |
49 | 42, 48 | mpbird 257 |
. 2
β’ ((π β§ π β β) β {π₯ β π΄ β£ (πΉβπ₯) < π} β (π΅ βΎt π΄)) |
50 | 1, 7, 16, 17, 49 | issmfd 45062 |
1
β’ (π β πΉ β (SMblFnβπ΅)) |