Step | Hyp | Ref
| Expression |
1 | | issmfgelem.i |
. . 3
β’ (π β π· β βͺ π) |
2 | | issmfgelem.f |
. . 3
β’ (π β πΉ:π·βΆβ) |
3 | | issmfgelem.s |
. . . . . . . . 9
β’ (π β π β SAlg) |
4 | 3, 1 | restuni4 43810 |
. . . . . . . 8
β’ (π β βͺ (π
βΎt π·) =
π·) |
5 | 4 | eqcomd 2739 |
. . . . . . 7
β’ (π β π· = βͺ (π βΎt π·)) |
6 | 5 | rabeqdv 3448 |
. . . . . 6
β’ (π β {π₯ β π· β£ (πΉβπ₯) < π} = {π₯ β βͺ (π βΎt π·) β£ (πΉβπ₯) < π}) |
7 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β {π₯ β π· β£ (πΉβπ₯) < π} = {π₯ β βͺ (π βΎt π·) β£ (πΉβπ₯) < π}) |
8 | | issmfgelem.x |
. . . . . . 7
β’
β²π₯π |
9 | | nfv 1918 |
. . . . . . 7
β’
β²π₯ π β β |
10 | 8, 9 | nfan 1903 |
. . . . . 6
β’
β²π₯(π β§ π β β) |
11 | | issmfgelem.a |
. . . . . . 7
β’
β²ππ |
12 | | nfv 1918 |
. . . . . . 7
β’
β²π π β β |
13 | 11, 12 | nfan 1903 |
. . . . . 6
β’
β²π(π β§ π β β) |
14 | 3 | uniexd 7732 |
. . . . . . . . . . 11
β’ (π β βͺ π
β V) |
15 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π· β βͺ π) β βͺ π
β V) |
16 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π· β βͺ π) β π· β βͺ π) |
17 | 15, 16 | ssexd 5325 |
. . . . . . . . 9
β’ ((π β§ π· β βͺ π) β π· β V) |
18 | 1, 17 | mpdan 686 |
. . . . . . . 8
β’ (π β π· β V) |
19 | | eqid 2733 |
. . . . . . . 8
β’ (π βΎt π·) = (π βΎt π·) |
20 | 3, 18, 19 | subsalsal 45075 |
. . . . . . 7
β’ (π β (π βΎt π·) β SAlg) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β (π βΎt π·) β SAlg) |
22 | | eqid 2733 |
. . . . . 6
β’ βͺ (π
βΎt π·) =
βͺ (π βΎt π·) |
23 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β βͺ (π βΎt π·)) β πΉ:π·βΆβ) |
24 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β βͺ (π βΎt π·)) β π₯ β βͺ (π βΎt π·)) |
25 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β βͺ (π βΎt π·)) β βͺ (π
βΎt π·) =
π·) |
26 | 24, 25 | eleqtrd 2836 |
. . . . . . . . 9
β’ ((π β§ π₯ β βͺ (π βΎt π·)) β π₯ β π·) |
27 | 23, 26 | ffvelcdmd 7088 |
. . . . . . . 8
β’ ((π β§ π₯ β βͺ (π βΎt π·)) β (πΉβπ₯) β β) |
28 | 27 | rexrd 11264 |
. . . . . . 7
β’ ((π β§ π₯ β βͺ (π βΎt π·)) β (πΉβπ₯) β
β*) |
29 | 28 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β βͺ (π βΎt π·)) β (πΉβπ₯) β
β*) |
30 | | issmfgelem.p |
. . . . . . . . . 10
β’ (π β βπ β β {π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·)) |
31 | 5 | rabeqdv 3448 |
. . . . . . . . . . . 12
β’ (π β {π₯ β π· β£ π β€ (πΉβπ₯)} = {π₯ β βͺ (π βΎt π·) β£ π β€ (πΉβπ₯)}) |
32 | 31 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π β ({π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·) β {π₯ β βͺ (π βΎt π·) β£ π β€ (πΉβπ₯)} β (π βΎt π·))) |
33 | 11, 32 | ralbid 3271 |
. . . . . . . . . 10
β’ (π β (βπ β β {π₯ β π· β£ π β€ (πΉβπ₯)} β (π βΎt π·) β βπ β β {π₯ β βͺ (π βΎt π·) β£ π β€ (πΉβπ₯)} β (π βΎt π·))) |
34 | 30, 33 | mpbid 231 |
. . . . . . . . 9
β’ (π β βπ β β {π₯ β βͺ (π βΎt π·) β£ π β€ (πΉβπ₯)} β (π βΎt π·)) |
35 | 34 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β βπ β β {π₯ β βͺ (π
βΎt π·)
β£ π β€ (πΉβπ₯)} β (π βΎt π·)) |
36 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
37 | | rspa 3246 |
. . . . . . . 8
β’
((βπ β
β {π₯ β βͺ (π
βΎt π·)
β£ π β€ (πΉβπ₯)} β (π βΎt π·) β§ π β β) β {π₯ β βͺ (π βΎt π·) β£ π β€ (πΉβπ₯)} β (π βΎt π·)) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β β) β {π₯ β βͺ (π βΎt π·) β£ π β€ (πΉβπ₯)} β (π βΎt π·)) |
39 | 38 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π β β) β {π₯ β βͺ (π βΎt π·) β£ π β€ (πΉβπ₯)} β (π βΎt π·)) |
40 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
41 | 10, 13, 21, 22, 29, 39, 40 | salpreimagelt 45423 |
. . . . 5
β’ ((π β§ π β β) β {π₯ β βͺ (π βΎt π·) β£ (πΉβπ₯) < π} β (π βΎt π·)) |
42 | 7, 41 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β β) β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)) |
43 | 42 | ralrimiva 3147 |
. . 3
β’ (π β βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)) |
44 | 1, 2, 43 | 3jca 1129 |
. 2
β’ (π β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·))) |
45 | | issmfgelem.d |
. . 3
β’ π· = dom πΉ |
46 | 3, 45 | issmf 45444 |
. 2
β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)))) |
47 | 44, 46 | mpbird 257 |
1
β’ (π β πΉ β (SMblFnβπ)) |