Step | Hyp | Ref
| Expression |
1 | | issmfle.s |
. . . . . . 7
β’ (π β π β SAlg) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (SMblFnβπ)) β π β SAlg) |
3 | | simpr 486 |
. . . . . 6
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ β (SMblFnβπ)) |
4 | | issmfle.d |
. . . . . 6
β’ π· = dom πΉ |
5 | 2, 3, 4 | smfdmss 45048 |
. . . . 5
β’ ((π β§ πΉ β (SMblFnβπ)) β π· β βͺ π) |
6 | 2, 3, 4 | smff 45047 |
. . . . 5
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ:π·βΆβ) |
7 | | nfv 1918 |
. . . . . . 7
β’
β²ππ |
8 | | nfv 1918 |
. . . . . . 7
β’
β²π πΉ β (SMblFnβπ) |
9 | 7, 8 | nfan 1903 |
. . . . . 6
β’
β²π(π β§ πΉ β (SMblFnβπ)) |
10 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦π |
11 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦ πΉ β (SMblFnβπ) |
12 | 10, 11 | nfan 1903 |
. . . . . . . . 9
β’
β²π¦(π β§ πΉ β (SMblFnβπ)) |
13 | | nfv 1918 |
. . . . . . . . 9
β’
β²π¦ π β β |
14 | 12, 13 | nfan 1903 |
. . . . . . . 8
β’
β²π¦((π β§ πΉ β (SMblFnβπ)) β§ π β β) |
15 | | nfv 1918 |
. . . . . . . 8
β’
β²π((π β§ πΉ β (SMblFnβπ)) β§ π β β) |
16 | 1 | uniexd 7684 |
. . . . . . . . . . . . 13
β’ (π β βͺ π
β V) |
17 | 16 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π· β βͺ π) β βͺ π
β V) |
18 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π· β βͺ π) β π· β βͺ π) |
19 | 17, 18 | ssexd 5286 |
. . . . . . . . . . 11
β’ ((π β§ π· β βͺ π) β π· β V) |
20 | 5, 19 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (SMblFnβπ)) β π· β V) |
21 | | eqid 2737 |
. . . . . . . . . 10
β’ (π βΎt π·) = (π βΎt π·) |
22 | 2, 20, 21 | subsalsal 44674 |
. . . . . . . . 9
β’ ((π β§ πΉ β (SMblFnβπ)) β (π βΎt π·) β SAlg) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β (π βΎt π·) β SAlg) |
24 | 6 | frexr 43693 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ:π·βΆβ*) |
25 | 24 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β πΉ:π·βΆβ*) |
26 | 25 | ffvelcdmda 7040 |
. . . . . . . 8
β’ ((((π β§ πΉ β (SMblFnβπ)) β§ π β β) β§ π¦ β π·) β (πΉβπ¦) β
β*) |
27 | 2 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β π β SAlg) |
28 | 3 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β πΉ β (SMblFnβπ)) |
29 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β π β β) |
30 | 27, 28, 4, 29 | smfpreimalt 45046 |
. . . . . . . . 9
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β {π¦ β π· β£ (πΉβπ¦) < π} β (π βΎt π·)) |
31 | 30 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ πΉ β (SMblFnβπ)) β§ π β β) β§ π β β) β {π¦ β π· β£ (πΉβπ¦) < π} β (π βΎt π·)) |
32 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β π β β) |
33 | 14, 15, 23, 26, 31, 32 | salpreimaltle 45041 |
. . . . . . 7
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) |
34 | 33 | ex 414 |
. . . . . 6
β’ ((π β§ πΉ β (SMblFnβπ)) β (π β β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·))) |
35 | 9, 34 | ralrimi 3243 |
. . . . 5
β’ ((π β§ πΉ β (SMblFnβπ)) β βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) |
36 | 5, 6, 35 | 3jca 1129 |
. . . 4
β’ ((π β§ πΉ β (SMblFnβπ)) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·))) |
37 | 36 | ex 414 |
. . 3
β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)))) |
38 | | nfv 1918 |
. . . . . . 7
β’
β²π¦ π· β βͺ π |
39 | | nfv 1918 |
. . . . . . 7
β’
β²π¦ πΉ:π·βΆβ |
40 | | nfcv 2908 |
. . . . . . . 8
β’
β²π¦β |
41 | | nfrab1 3429 |
. . . . . . . . 9
β’
β²π¦{π¦ β π· β£ (πΉβπ¦) β€ π} |
42 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π¦(π βΎt π·) |
43 | 41, 42 | nfel 2922 |
. . . . . . . 8
β’
β²π¦{π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·) |
44 | 40, 43 | nfralw 3297 |
. . . . . . 7
β’
β²π¦βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·) |
45 | 38, 39, 44 | nf3an 1905 |
. . . . . 6
β’
β²π¦(π· β βͺ π
β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) |
46 | 10, 45 | nfan 1903 |
. . . . 5
β’
β²π¦(π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·))) |
47 | | nfv 1918 |
. . . . . . 7
β’
β²π π· β βͺ π |
48 | | nfv 1918 |
. . . . . . 7
β’
β²π πΉ:π·βΆβ |
49 | | nfra1 3270 |
. . . . . . 7
β’
β²πβπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·) |
50 | 47, 48, 49 | nf3an 1905 |
. . . . . 6
β’
β²π(π· β βͺ π
β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) |
51 | 7, 50 | nfan 1903 |
. . . . 5
β’
β²π(π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·))) |
52 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·))) β π β SAlg) |
53 | | simpr1 1195 |
. . . . 5
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·))) β π· β βͺ π) |
54 | | simpr2 1196 |
. . . . 5
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·))) β πΉ:π·βΆβ) |
55 | | rspa 3234 |
. . . . . . 7
β’
((βπ β
β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·) β§ π β β) β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) |
56 | 55 | 3ad2antl3 1188 |
. . . . . 6
β’ (((π· β βͺ π
β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) β§ π β β) β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) |
57 | 56 | adantll 713 |
. . . . 5
β’ (((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·))) β§ π β β) β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) |
58 | 46, 51, 52, 4, 53, 54, 57 | issmflelem 45059 |
. . . 4
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·))) β πΉ β (SMblFnβπ)) |
59 | 58 | ex 414 |
. . 3
β’ (π β ((π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) β πΉ β (SMblFnβπ))) |
60 | 37, 59 | impbid 211 |
. 2
β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)))) |
61 | | breq2 5114 |
. . . . . . . 8
β’ (π = π β ((πΉβπ¦) β€ π β (πΉβπ¦) β€ π)) |
62 | 61 | rabbidv 3418 |
. . . . . . 7
β’ (π = π β {π¦ β π· β£ (πΉβπ¦) β€ π} = {π¦ β π· β£ (πΉβπ¦) β€ π}) |
63 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (πΉβπ¦) = (πΉβπ₯)) |
64 | 63 | breq1d 5120 |
. . . . . . . . 9
β’ (π¦ = π₯ β ((πΉβπ¦) β€ π β (πΉβπ₯) β€ π)) |
65 | 64 | cbvrabv 3420 |
. . . . . . . 8
β’ {π¦ β π· β£ (πΉβπ¦) β€ π} = {π₯ β π· β£ (πΉβπ₯) β€ π} |
66 | 65 | a1i 11 |
. . . . . . 7
β’ (π = π β {π¦ β π· β£ (πΉβπ¦) β€ π} = {π₯ β π· β£ (πΉβπ₯) β€ π}) |
67 | 62, 66 | eqtrd 2777 |
. . . . . 6
β’ (π = π β {π¦ β π· β£ (πΉβπ¦) β€ π} = {π₯ β π· β£ (πΉβπ₯) β€ π}) |
68 | 67 | eleq1d 2823 |
. . . . 5
β’ (π = π β ({π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·) β {π₯ β π· β£ (πΉβπ₯) β€ π} β (π βΎt π·))) |
69 | 68 | cbvralvw 3228 |
. . . 4
β’
(βπ β
β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·) β βπ β β {π₯ β π· β£ (πΉβπ₯) β€ π} β (π βΎt π·)) |
70 | 69 | 3anbi3i 1160 |
. . 3
β’ ((π· β βͺ π
β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) β€ π} β (π βΎt π·))) |
71 | 70 | a1i 11 |
. 2
β’ (π β ((π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π¦ β π· β£ (πΉβπ¦) β€ π} β (π βΎt π·)) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) β€ π} β (π βΎt π·)))) |
72 | 60, 71 | bitrd 279 |
1
β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) β€ π} β (π βΎt π·)))) |