Step | Hyp | Ref
| Expression |
1 | | smfconst.f |
. . 3
β’ πΉ = (π₯ β π΄ β¦ π΅) |
2 | | nfmpt1 5214 |
. . 3
β’
β²π₯(π₯ β π΄ β¦ π΅) |
3 | 1, 2 | nfcxfr 2902 |
. 2
β’
β²π₯πΉ |
4 | | nfv 1918 |
. 2
β’
β²ππ |
5 | | smfconst.s |
. 2
β’ (π β π β SAlg) |
6 | | smfconst.a |
. 2
β’ (π β π΄ β βͺ π) |
7 | | smfconst.x |
. . 3
β’
β²π₯π |
8 | | smfconst.b |
. . . 4
β’ (π β π΅ β β) |
9 | 8 | adantr 482 |
. . 3
β’ ((π β§ π₯ β π΄) β π΅ β β) |
10 | 7, 9, 1 | fmptdf 7066 |
. 2
β’ (π β πΉ:π΄βΆβ) |
11 | | nfv 1918 |
. . . . . . . 8
β’
β²π₯ π β β |
12 | 7, 11 | nfan 1903 |
. . . . . . 7
β’
β²π₯(π β§ π β β) |
13 | | nfv 1918 |
. . . . . . 7
β’
β²π₯ π΅ < π |
14 | 12, 13 | nfan 1903 |
. . . . . 6
β’
β²π₯((π β§ π β β) β§ π΅ < π) |
15 | 8 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ π΅ < π) β π΅ β β) |
16 | | simpr 486 |
. . . . . 6
β’ (((π β§ π β β) β§ π΅ < π) β π΅ < π) |
17 | 14, 15, 1, 16 | pimconstlt1 45029 |
. . . . 5
β’ (((π β§ π β β) β§ π΅ < π) β {π₯ β π΄ β£ (πΉβπ₯) < π} = π΄) |
18 | | eqidd 2734 |
. . . . 5
β’ (((π β§ π β β) β§ π΅ < π) β π΄ = π΄) |
19 | | sseqin2 4176 |
. . . . . . . 8
β’ (π΄ β βͺ π
β (βͺ π β© π΄) = π΄) |
20 | 6, 19 | sylib 217 |
. . . . . . 7
β’ (π β (βͺ π
β© π΄) = π΄) |
21 | 20 | eqcomd 2739 |
. . . . . 6
β’ (π β π΄ = (βͺ π β© π΄)) |
22 | 21 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β) β§ π΅ < π) β π΄ = (βͺ π β© π΄)) |
23 | 17, 18, 22 | 3eqtrd 2777 |
. . . 4
β’ (((π β§ π β β) β§ π΅ < π) β {π₯ β π΄ β£ (πΉβπ₯) < π} = (βͺ π β© π΄)) |
24 | 5 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β) β§ π΅ < π) β π β SAlg) |
25 | 5 | uniexd 7680 |
. . . . . . 7
β’ (π β βͺ π
β V) |
26 | 25, 6 | ssexd 5282 |
. . . . . 6
β’ (π β π΄ β V) |
27 | 26 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β) β§ π΅ < π) β π΄ β V) |
28 | 24 | salunid 44680 |
. . . . 5
β’ (((π β§ π β β) β§ π΅ < π) β βͺ π β π) |
29 | | eqid 2733 |
. . . . 5
β’ (βͺ π
β© π΄) = (βͺ π
β© π΄) |
30 | 24, 27, 28, 29 | elrestd 43406 |
. . . 4
β’ (((π β§ π β β) β§ π΅ < π) β (βͺ π β© π΄) β (π βΎt π΄)) |
31 | 23, 30 | eqeltrd 2834 |
. . 3
β’ (((π β§ π β β) β§ π΅ < π) β {π₯ β π΄ β£ (πΉβπ₯) < π} β (π βΎt π΄)) |
32 | | nfv 1918 |
. . . . . 6
β’
β²π₯ Β¬ π΅ < π |
33 | 12, 32 | nfan 1903 |
. . . . 5
β’
β²π₯((π β§ π β β) β§ Β¬ π΅ < π) |
34 | 8 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β) β§ Β¬ π΅ < π) β π΅ β β) |
35 | | rexr 11206 |
. . . . . 6
β’ (π β β β π β
β*) |
36 | 35 | ad2antlr 726 |
. . . . 5
β’ (((π β§ π β β) β§ Β¬ π΅ < π) β π β β*) |
37 | | simpr 486 |
. . . . . 6
β’ (((π β§ π β β) β§ Β¬ π΅ < π) β Β¬ π΅ < π) |
38 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π β β) β§ Β¬ π΅ < π) β π β β) |
39 | 38, 34 | lenltd 11306 |
. . . . . 6
β’ (((π β§ π β β) β§ Β¬ π΅ < π) β (π β€ π΅ β Β¬ π΅ < π)) |
40 | 37, 39 | mpbird 257 |
. . . . 5
β’ (((π β§ π β β) β§ Β¬ π΅ < π) β π β€ π΅) |
41 | 33, 34, 1, 36, 40 | pimconstlt0 45028 |
. . . 4
β’ (((π β§ π β β) β§ Β¬ π΅ < π) β {π₯ β π΄ β£ (πΉβπ₯) < π} = β
) |
42 | | eqid 2733 |
. . . . . . 7
β’ (π βΎt π΄) = (π βΎt π΄) |
43 | 5, 26, 42 | subsalsal 44686 |
. . . . . 6
β’ (π β (π βΎt π΄) β SAlg) |
44 | 43 | 0sald 44677 |
. . . . 5
β’ (π β β
β (π βΎt π΄)) |
45 | 44 | ad2antrr 725 |
. . . 4
β’ (((π β§ π β β) β§ Β¬ π΅ < π) β β
β (π βΎt π΄)) |
46 | 41, 45 | eqeltrd 2834 |
. . 3
β’ (((π β§ π β β) β§ Β¬ π΅ < π) β {π₯ β π΄ β£ (πΉβπ₯) < π} β (π βΎt π΄)) |
47 | 31, 46 | pm2.61dan 812 |
. 2
β’ ((π β§ π β β) β {π₯ β π΄ β£ (πΉβπ₯) < π} β (π βΎt π΄)) |
48 | 3, 4, 5, 6, 10, 47 | issmfdf 45064 |
1
β’ (π β πΉ β (SMblFnβπ)) |