Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . 7
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ β (SMblFnβπ)) |
2 | | df-smblfn 45011 |
. . . . . . . . 9
β’ SMblFn =
(π β SAlg β¦
{π β (β
βpm βͺ π ) β£ βπ β β (β‘π β (-β(,)π)) β (π βΎt dom π)}) |
3 | | unieq 4881 |
. . . . . . . . . . . 12
β’ (π = π β βͺ π = βͺ
π) |
4 | 3 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β (β βpm βͺ π ) =
(β βpm βͺ π)) |
5 | 4 | rabeqdv 3425 |
. . . . . . . . . 10
β’ (π = π β {π β (β βpm βͺ π )
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)} = {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)}) |
6 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π = π β (π βΎt dom π) = (π βΎt dom π)) |
7 | 6 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ (π = π β ((β‘π β (-β(,)π)) β (π βΎt dom π) β (β‘π β (-β(,)π)) β (π βΎt dom π))) |
8 | 7 | ralbidv 3175 |
. . . . . . . . . . 11
β’ (π = π β (βπ β β (β‘π β (-β(,)π)) β (π βΎt dom π) β βπ β β (β‘π β (-β(,)π)) β (π βΎt dom π))) |
9 | 8 | rabbidv 3418 |
. . . . . . . . . 10
β’ (π = π β {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)} = {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)}) |
10 | 5, 9 | eqtrd 2777 |
. . . . . . . . 9
β’ (π = π β {π β (β βpm βͺ π )
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)} = {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)}) |
11 | | issmflem.s |
. . . . . . . . 9
β’ (π β π β SAlg) |
12 | | ovex 7395 |
. . . . . . . . . . 11
β’ (β
βpm βͺ π) β V |
13 | 12 | rabex 5294 |
. . . . . . . . . 10
β’ {π β (β
βpm βͺ π) β£ βπ β β (β‘π β (-β(,)π)) β (π βΎt dom π)} β V |
14 | 13 | a1i 11 |
. . . . . . . . 9
β’ (π β {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)} β V) |
15 | 2, 10, 11, 14 | fvmptd3 6976 |
. . . . . . . 8
β’ (π β (SMblFnβπ) = {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)}) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΉ β (SMblFnβπ)) β (SMblFnβπ) = {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)}) |
17 | 1, 16 | eleqtrd 2840 |
. . . . . 6
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ β {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)}) |
18 | | elrabi 3644 |
. . . . . 6
β’ (πΉ β {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)} β πΉ β (β βpm βͺ π)) |
19 | 17, 18 | syl 17 |
. . . . 5
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ β (β βpm βͺ π)) |
20 | | issmflem.d |
. . . . . . 7
β’ π· = dom πΉ |
21 | | elpmi2 43520 |
. . . . . . 7
β’ (πΉ β (β
βpm βͺ π) β dom πΉ β βͺ π) |
22 | 20, 21 | eqsstrid 3997 |
. . . . . 6
β’ (πΉ β (β
βpm βͺ π) β π· β βͺ π) |
23 | 22 | adantl 483 |
. . . . 5
β’ ((π β§ πΉ β (β βpm βͺ π))
β π· β βͺ π) |
24 | 19, 23 | syldan 592 |
. . . 4
β’ ((π β§ πΉ β (SMblFnβπ)) β π· β βͺ π) |
25 | | elpmi 8791 |
. . . . . . 7
β’ (πΉ β (β
βpm βͺ π) β (πΉ:dom πΉβΆβ β§ dom πΉ β βͺ π)) |
26 | 19, 25 | syl 17 |
. . . . . 6
β’ ((π β§ πΉ β (SMblFnβπ)) β (πΉ:dom πΉβΆβ β§ dom πΉ β βͺ π)) |
27 | 26 | simpld 496 |
. . . . 5
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ:dom πΉβΆβ) |
28 | 20 | feq2i 6665 |
. . . . . 6
β’ (πΉ:π·βΆβ β πΉ:dom πΉβΆβ) |
29 | 28 | a1i 11 |
. . . . 5
β’ ((π β§ πΉ β (SMblFnβπ)) β (πΉ:π·βΆβ β πΉ:dom πΉβΆβ)) |
30 | 27, 29 | mpbird 257 |
. . . 4
β’ ((π β§ πΉ β (SMblFnβπ)) β πΉ:π·βΆβ) |
31 | | cnveq 5834 |
. . . . . . . . . . . . . 14
β’ (π = πΉ β β‘π = β‘πΉ) |
32 | 31 | imaeq1d 6017 |
. . . . . . . . . . . . 13
β’ (π = πΉ β (β‘π β (-β(,)π)) = (β‘πΉ β (-β(,)π))) |
33 | | dmeq 5864 |
. . . . . . . . . . . . . 14
β’ (π = πΉ β dom π = dom πΉ) |
34 | 33 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π = πΉ β (π βΎt dom π) = (π βΎt dom πΉ)) |
35 | 32, 34 | eleq12d 2832 |
. . . . . . . . . . . 12
β’ (π = πΉ β ((β‘π β (-β(,)π)) β (π βΎt dom π) β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ))) |
36 | 35 | ralbidv 3175 |
. . . . . . . . . . 11
β’ (π = πΉ β (βπ β β (β‘π β (-β(,)π)) β (π βΎt dom π) β βπ β β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ))) |
37 | 36 | elrab 3650 |
. . . . . . . . . 10
β’ (πΉ β {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)} β (πΉ β (β βpm βͺ π)
β§ βπ β
β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ))) |
38 | 37 | simprbi 498 |
. . . . . . . . 9
β’ (πΉ β {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)} β βπ β β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ)) |
39 | 17, 38 | syl 17 |
. . . . . . . 8
β’ ((π β§ πΉ β (SMblFnβπ)) β βπ β β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ)) |
40 | 39 | adantr 482 |
. . . . . . 7
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β βπ β β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ)) |
41 | | simpr 486 |
. . . . . . 7
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β π β β) |
42 | | rspa 3234 |
. . . . . . 7
β’
((βπ β
β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ) β§ π β β) β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ)) |
43 | 40, 41, 42 | syl2anc 585 |
. . . . . 6
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ)) |
44 | 30 | adantr 482 |
. . . . . . . 8
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β πΉ:π·βΆβ) |
45 | | simpl 484 |
. . . . . . . . . 10
β’ ((πΉ:π·βΆβ β§ π β β) β πΉ:π·βΆβ) |
46 | | simpr 486 |
. . . . . . . . . . 11
β’ ((πΉ:π·βΆβ β§ π β β) β π β β) |
47 | 46 | rexrd 11212 |
. . . . . . . . . 10
β’ ((πΉ:π·βΆβ β§ π β β) β π β β*) |
48 | 45, 47 | preimaioomnf 45034 |
. . . . . . . . 9
β’ ((πΉ:π·βΆβ β§ π β β) β (β‘πΉ β (-β(,)π)) = {π₯ β π· β£ (πΉβπ₯) < π}) |
49 | 48 | eqcomd 2743 |
. . . . . . . 8
β’ ((πΉ:π·βΆβ β§ π β β) β {π₯ β π· β£ (πΉβπ₯) < π} = (β‘πΉ β (-β(,)π))) |
50 | 44, 41, 49 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β {π₯ β π· β£ (πΉβπ₯) < π} = (β‘πΉ β (-β(,)π))) |
51 | 20 | oveq2i 7373 |
. . . . . . . 8
β’ (π βΎt π·) = (π βΎt dom πΉ) |
52 | 51 | a1i 11 |
. . . . . . 7
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β (π βΎt π·) = (π βΎt dom πΉ)) |
53 | 50, 52 | eleq12d 2832 |
. . . . . 6
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β ({π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·) β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ))) |
54 | 43, 53 | mpbird 257 |
. . . . 5
β’ (((π β§ πΉ β (SMblFnβπ)) β§ π β β) β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)) |
55 | 54 | ralrimiva 3144 |
. . . 4
β’ ((π β§ πΉ β (SMblFnβπ)) β βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)) |
56 | 24, 30, 55 | 3jca 1129 |
. . 3
β’ ((π β§ πΉ β (SMblFnβπ)) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·))) |
57 | 56 | ex 414 |
. 2
β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)))) |
58 | | reex 11149 |
. . . . . . . . 9
β’ β
β V |
59 | 58 | a1i 11 |
. . . . . . . 8
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ)) β β β
V) |
60 | 11 | uniexd 7684 |
. . . . . . . . 9
β’ (π β βͺ π
β V) |
61 | 60 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ)) β βͺ π
β V) |
62 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ)) β πΉ:π·βΆβ) |
63 | | fssxp 6701 |
. . . . . . . . . . . 12
β’ (πΉ:π·βΆβ β πΉ β (π· Γ β)) |
64 | 63 | adantl 483 |
. . . . . . . . . . 11
β’ ((π· β βͺ π
β§ πΉ:π·βΆβ) β πΉ β (π· Γ β)) |
65 | | xpss1 5657 |
. . . . . . . . . . . 12
β’ (π· β βͺ π
β (π· Γ β)
β (βͺ π Γ β)) |
66 | 65 | adantr 482 |
. . . . . . . . . . 11
β’ ((π· β βͺ π
β§ πΉ:π·βΆβ) β (π· Γ β) β (βͺ π
Γ β)) |
67 | 64, 66 | sstrd 3959 |
. . . . . . . . . 10
β’ ((π· β βͺ π
β§ πΉ:π·βΆβ) β πΉ β (βͺ π Γ
β)) |
68 | 67 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ)) β πΉ β (βͺ π Γ
β)) |
69 | | dmss 5863 |
. . . . . . . . . . . 12
β’ (πΉ β (βͺ π
Γ β) β dom πΉ β dom (βͺ
π Γ
β)) |
70 | | dmxpss 6128 |
. . . . . . . . . . . . 13
β’ dom
(βͺ π Γ β) β βͺ π |
71 | 70 | a1i 11 |
. . . . . . . . . . . 12
β’ (πΉ β (βͺ π
Γ β) β dom (βͺ π Γ β) β βͺ π) |
72 | 69, 71 | sstrd 3959 |
. . . . . . . . . . 11
β’ (πΉ β (βͺ π
Γ β) β dom πΉ β βͺ π) |
73 | 72 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (βͺ π Γ β)) β dom
πΉ β βͺ π) |
74 | 20, 73 | eqsstrid 3997 |
. . . . . . . . 9
β’ ((π β§ πΉ β (βͺ π Γ β)) β π· β βͺ π) |
75 | 68, 74 | syldan 592 |
. . . . . . . 8
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ)) β π· β βͺ π) |
76 | | elpm2r 8790 |
. . . . . . . 8
β’
(((β β V β§ βͺ π β V) β§ (πΉ:π·βΆβ β§ π· β βͺ π)) β πΉ β (β βpm βͺ π)) |
77 | 59, 61, 62, 75, 76 | syl22anc 838 |
. . . . . . 7
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ)) β πΉ β (β βpm βͺ π)) |
78 | 77 | 3adantr3 1172 |
. . . . . 6
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·))) β πΉ β (β βpm βͺ π)) |
79 | 20 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((πΉ:π·βΆβ β§ π β β) β π· = dom πΉ) |
80 | 79 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((πΉ:π·βΆβ β§ π β β) β (π βΎt π·) = (π βΎt dom πΉ)) |
81 | 49, 80 | eleq12d 2832 |
. . . . . . . . . . 11
β’ ((πΉ:π·βΆβ β§ π β β) β ({π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·) β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ))) |
82 | 81 | ralbidva 3173 |
. . . . . . . . . 10
β’ (πΉ:π·βΆβ β (βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·) β βπ β β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ))) |
83 | 82 | biimpd 228 |
. . . . . . . . 9
β’ (πΉ:π·βΆβ β (βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·) β βπ β β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ))) |
84 | 83 | imp 408 |
. . . . . . . 8
β’ ((πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)) β βπ β β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ)) |
85 | 84 | adantl 483 |
. . . . . . 7
β’ ((π β§ (πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·))) β βπ β β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ)) |
86 | 85 | 3adantr1 1170 |
. . . . . 6
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·))) β βπ β β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ)) |
87 | 78, 86 | jca 513 |
. . . . 5
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·))) β (πΉ β (β βpm βͺ π)
β§ βπ β
β (β‘πΉ β (-β(,)π)) β (π βΎt dom πΉ))) |
88 | 87, 37 | sylibr 233 |
. . . 4
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·))) β πΉ β {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)}) |
89 | 15 | eqcomd 2743 |
. . . . 5
β’ (π β {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)} = (SMblFnβπ)) |
90 | 89 | adantr 482 |
. . . 4
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·))) β {π β (β βpm βͺ π)
β£ βπ β
β (β‘π β (-β(,)π)) β (π βΎt dom π)} = (SMblFnβπ)) |
91 | 88, 90 | eleqtrd 2840 |
. . 3
β’ ((π β§ (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·))) β πΉ β (SMblFnβπ)) |
92 | 91 | ex 414 |
. 2
β’ (π β ((π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)) β πΉ β (SMblFnβπ))) |
93 | 57, 92 | impbid 211 |
1
β’ (π β (πΉ β (SMblFnβπ) β (π· β βͺ π β§ πΉ:π·βΆβ β§ βπ β β {π₯ β π· β£ (πΉβπ₯) < π} β (π βΎt π·)))) |