Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. 2
β’
β²ππ |
2 | | sssmf.s |
. 2
β’ (π β π β SAlg) |
3 | | inss2 4190 |
. . 3
β’ (π΅ β© dom πΉ) β dom πΉ |
4 | | sssmf.f |
. . . 4
β’ (π β πΉ β (SMblFnβπ)) |
5 | | eqid 2733 |
. . . 4
β’ dom πΉ = dom πΉ |
6 | 2, 4, 5 | smfdmss 45060 |
. . 3
β’ (π β dom πΉ β βͺ π) |
7 | 3, 6 | sstrid 3956 |
. 2
β’ (π β (π΅ β© dom πΉ) β βͺ π) |
8 | 2, 4, 5 | smff 45059 |
. . . . 5
β’ (π β πΉ:dom πΉβΆβ) |
9 | 3 | a1i 11 |
. . . . 5
β’ (π β (π΅ β© dom πΉ) β dom πΉ) |
10 | | fssres 6709 |
. . . . 5
β’ ((πΉ:dom πΉβΆβ β§ (π΅ β© dom πΉ) β dom πΉ) β (πΉ βΎ (π΅ β© dom πΉ)):(π΅ β© dom πΉ)βΆβ) |
11 | 8, 9, 10 | syl2anc 585 |
. . . 4
β’ (π β (πΉ βΎ (π΅ β© dom πΉ)):(π΅ β© dom πΉ)βΆβ) |
12 | 8 | freld 6675 |
. . . . . . 7
β’ (π β Rel πΉ) |
13 | | resindm 5987 |
. . . . . . 7
β’ (Rel
πΉ β (πΉ βΎ (π΅ β© dom πΉ)) = (πΉ βΎ π΅)) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ (π β (πΉ βΎ (π΅ β© dom πΉ)) = (πΉ βΎ π΅)) |
15 | 14 | eqcomd 2739 |
. . . . 5
β’ (π β (πΉ βΎ π΅) = (πΉ βΎ (π΅ β© dom πΉ))) |
16 | | dmres 5960 |
. . . . . 6
β’ dom
(πΉ βΎ π΅) = (π΅ β© dom πΉ) |
17 | 16 | a1i 11 |
. . . . 5
β’ (π β dom (πΉ βΎ π΅) = (π΅ β© dom πΉ)) |
18 | 15, 17 | feq12d 6657 |
. . . 4
β’ (π β ((πΉ βΎ π΅):dom (πΉ βΎ π΅)βΆβ β (πΉ βΎ (π΅ β© dom πΉ)):(π΅ β© dom πΉ)βΆβ)) |
19 | 11, 18 | mpbird 257 |
. . 3
β’ (π β (πΉ βΎ π΅):dom (πΉ βΎ π΅)βΆβ) |
20 | 17 | feq2d 6655 |
. . 3
β’ (π β ((πΉ βΎ π΅):dom (πΉ βΎ π΅)βΆβ β (πΉ βΎ π΅):(π΅ β© dom πΉ)βΆβ)) |
21 | 19, 20 | mpbid 231 |
. 2
β’ (π β (πΉ βΎ π΅):(π΅ β© dom πΉ)βΆβ) |
22 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β π β SAlg) |
23 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β πΉ β (SMblFnβπ)) |
24 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
25 | 22, 23, 5, 24 | smfpreimalt 45058 |
. . . 4
β’ ((π β§ π β β) β {π₯ β dom πΉ β£ (πΉβπ₯) < π} β (π βΎt dom πΉ)) |
26 | 4 | dmexd 7843 |
. . . . . 6
β’ (π β dom πΉ β V) |
27 | | elrest 17314 |
. . . . . 6
β’ ((π β SAlg β§ dom πΉ β V) β ({π₯ β dom πΉ β£ (πΉβπ₯) < π} β (π βΎt dom πΉ) β βπ€ β π {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ))) |
28 | 2, 26, 27 | syl2anc 585 |
. . . . 5
β’ (π β ({π₯ β dom πΉ β£ (πΉβπ₯) < π} β (π βΎt dom πΉ) β βπ€ β π {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ))) |
29 | 28 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β ({π₯ β dom πΉ β£ (πΉβπ₯) < π} β (π βΎt dom πΉ) β βπ€ β π {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ))) |
30 | 25, 29 | mpbid 231 |
. . 3
β’ ((π β§ π β β) β βπ€ β π {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) |
31 | | elinel1 4156 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΅ β© dom πΉ) β π₯ β π΅) |
32 | 31 | fvresd 6863 |
. . . . . . . . . . . 12
β’ (π₯ β (π΅ β© dom πΉ) β ((πΉ βΎ π΅)βπ₯) = (πΉβπ₯)) |
33 | 32 | breq1d 5116 |
. . . . . . . . . . 11
β’ (π₯ β (π΅ β© dom πΉ) β (((πΉ βΎ π΅)βπ₯) < π β (πΉβπ₯) < π)) |
34 | 33 | rabbiia 3410 |
. . . . . . . . . 10
β’ {π₯ β (π΅ β© dom πΉ) β£ ((πΉ βΎ π΅)βπ₯) < π} = {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} |
35 | 34 | a1i 11 |
. . . . . . . . 9
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β (π΅ β© dom πΉ) β£ ((πΉ βΎ π΅)βπ₯) < π} = {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π}) |
36 | | rabss2 4036 |
. . . . . . . . . . . . 13
β’ ((π΅ β© dom πΉ) β dom πΉ β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} β {π₯ β dom πΉ β£ (πΉβπ₯) < π}) |
37 | 3, 36 | ax-mp 5 |
. . . . . . . . . . . 12
β’ {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} β {π₯ β dom πΉ β£ (πΉβπ₯) < π} |
38 | | id 22 |
. . . . . . . . . . . . 13
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) |
39 | | inss1 4189 |
. . . . . . . . . . . . . 14
β’ (π€ β© dom πΉ) β π€ |
40 | 39 | a1i 11 |
. . . . . . . . . . . . 13
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β (π€ β© dom πΉ) β π€) |
41 | 38, 40 | eqsstrd 3983 |
. . . . . . . . . . . 12
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β dom πΉ β£ (πΉβπ₯) < π} β π€) |
42 | 37, 41 | sstrid 3956 |
. . . . . . . . . . 11
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} β π€) |
43 | | ssrab2 4038 |
. . . . . . . . . . . 12
β’ {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} β (π΅ β© dom πΉ) |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} β (π΅ β© dom πΉ)) |
45 | 42, 44 | ssind 4193 |
. . . . . . . . . 10
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} β (π€ β© (π΅ β© dom πΉ))) |
46 | | nfrab1 3425 |
. . . . . . . . . . . . 13
β’
β²π₯{π₯ β dom πΉ β£ (πΉβπ₯) < π} |
47 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π₯(π€ β© dom πΉ) |
48 | 46, 47 | nfeq 2917 |
. . . . . . . . . . . 12
β’
β²π₯{π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) |
49 | | elinel2 4157 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (π€ β© (π΅ β© dom πΉ)) β π₯ β (π΅ β© dom πΉ)) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β§ π₯ β (π€ β© (π΅ β© dom πΉ))) β π₯ β (π΅ β© dom πΉ)) |
51 | | elinel1 4156 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (π€ β© (π΅ β© dom πΉ)) β π₯ β π€) |
52 | 3 | sseli 3941 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β (π΅ β© dom πΉ) β π₯ β dom πΉ) |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (π€ β© (π΅ β© dom πΉ)) β π₯ β dom πΉ) |
54 | 51, 53 | elind 4155 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β (π€ β© (π΅ β© dom πΉ)) β π₯ β (π€ β© dom πΉ)) |
55 | 54 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β§ π₯ β (π€ β© (π΅ β© dom πΉ))) β π₯ β (π€ β© dom πΉ)) |
56 | 38 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β (π€ β© dom πΉ) = {π₯ β dom πΉ β£ (πΉβπ₯) < π}) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β§ π₯ β (π€ β© (π΅ β© dom πΉ))) β (π€ β© dom πΉ) = {π₯ β dom πΉ β£ (πΉβπ₯) < π}) |
58 | 55, 57 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . 19
β’ (({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β§ π₯ β (π€ β© (π΅ β© dom πΉ))) β π₯ β {π₯ β dom πΉ β£ (πΉβπ₯) < π}) |
59 | | rabid 3426 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β {π₯ β dom πΉ β£ (πΉβπ₯) < π} β (π₯ β dom πΉ β§ (πΉβπ₯) < π)) |
60 | 59 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β {π₯ β dom πΉ β£ (πΉβπ₯) < π} β (π₯ β dom πΉ β§ (πΉβπ₯) < π)) |
61 | 60 | simprd 497 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β {π₯ β dom πΉ β£ (πΉβπ₯) < π} β (πΉβπ₯) < π) |
62 | 58, 61 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β§ π₯ β (π€ β© (π΅ β© dom πΉ))) β (πΉβπ₯) < π) |
63 | 50, 62 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ (({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β§ π₯ β (π€ β© (π΅ β© dom πΉ))) β (π₯ β (π΅ β© dom πΉ) β§ (πΉβπ₯) < π)) |
64 | | rabid 3426 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} β (π₯ β (π΅ β© dom πΉ) β§ (πΉβπ₯) < π)) |
65 | 63, 64 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β§ π₯ β (π€ β© (π΅ β© dom πΉ))) β π₯ β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π}) |
66 | 65 | ex 414 |
. . . . . . . . . . . . . . 15
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β (π₯ β (π€ β© (π΅ β© dom πΉ)) β π₯ β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π})) |
67 | 48, 66 | ralrimi 3239 |
. . . . . . . . . . . . . 14
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β βπ₯ β (π€ β© (π΅ β© dom πΉ))π₯ β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π}) |
68 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²π₯(π€ β© (π΅ β© dom πΉ)) |
69 | | nfrab1 3425 |
. . . . . . . . . . . . . . 15
β’
β²π₯{π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} |
70 | 68, 69 | dfss3f 3936 |
. . . . . . . . . . . . . 14
β’ ((π€ β© (π΅ β© dom πΉ)) β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} β βπ₯ β (π€ β© (π΅ β© dom πΉ))π₯ β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π}) |
71 | 67, 70 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β (π€ β© (π΅ β© dom πΉ)) β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π}) |
72 | 71 | sseld 3944 |
. . . . . . . . . . . 12
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β (π₯ β (π€ β© (π΅ β© dom πΉ)) β π₯ β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π})) |
73 | 48, 72 | ralrimi 3239 |
. . . . . . . . . . 11
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β βπ₯ β (π€ β© (π΅ β© dom πΉ))π₯ β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π}) |
74 | 73, 70 | sylibr 233 |
. . . . . . . . . 10
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β (π€ β© (π΅ β© dom πΉ)) β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π}) |
75 | 45, 74 | eqssd 3962 |
. . . . . . . . 9
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β (π΅ β© dom πΉ) β£ (πΉβπ₯) < π} = (π€ β© (π΅ β© dom πΉ))) |
76 | 35, 75 | eqtrd 2773 |
. . . . . . . 8
β’ ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β (π΅ β© dom πΉ) β£ ((πΉ βΎ π΅)βπ₯) < π} = (π€ β© (π΅ β© dom πΉ))) |
77 | 76 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β) β§ {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) β {π₯ β (π΅ β© dom πΉ) β£ ((πΉ βΎ π΅)βπ₯) < π} = (π€ β© (π΅ β© dom πΉ))) |
78 | 77 | 3adant2 1132 |
. . . . . 6
β’ (((π β§ π β β) β§ π€ β π β§ {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) β {π₯ β (π΅ β© dom πΉ) β£ ((πΉ βΎ π΅)βπ₯) < π} = (π€ β© (π΅ β© dom πΉ))) |
79 | 22 | 3ad2ant1 1134 |
. . . . . . 7
β’ (((π β§ π β β) β§ π€ β π β§ {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) β π β SAlg) |
80 | | simp1l 1198 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π€ β π β§ {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) β π) |
81 | 26, 9 | ssexd 5282 |
. . . . . . . 8
β’ (π β (π΅ β© dom πΉ) β V) |
82 | 80, 81 | syl 17 |
. . . . . . 7
β’ (((π β§ π β β) β§ π€ β π β§ {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) β (π΅ β© dom πΉ) β V) |
83 | | simp2 1138 |
. . . . . . 7
β’ (((π β§ π β β) β§ π€ β π β§ {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) β π€ β π) |
84 | | eqid 2733 |
. . . . . . 7
β’ (π€ β© (π΅ β© dom πΉ)) = (π€ β© (π΅ β© dom πΉ)) |
85 | 79, 82, 83, 84 | elrestd 43406 |
. . . . . 6
β’ (((π β§ π β β) β§ π€ β π β§ {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) β (π€ β© (π΅ β© dom πΉ)) β (π βΎt (π΅ β© dom πΉ))) |
86 | 78, 85 | eqeltrd 2834 |
. . . . 5
β’ (((π β§ π β β) β§ π€ β π β§ {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ)) β {π₯ β (π΅ β© dom πΉ) β£ ((πΉ βΎ π΅)βπ₯) < π} β (π βΎt (π΅ β© dom πΉ))) |
87 | 86 | 3exp 1120 |
. . . 4
β’ ((π β§ π β β) β (π€ β π β ({π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β (π΅ β© dom πΉ) β£ ((πΉ βΎ π΅)βπ₯) < π} β (π βΎt (π΅ β© dom πΉ))))) |
88 | 87 | rexlimdv 3147 |
. . 3
β’ ((π β§ π β β) β (βπ€ β π {π₯ β dom πΉ β£ (πΉβπ₯) < π} = (π€ β© dom πΉ) β {π₯ β (π΅ β© dom πΉ) β£ ((πΉ βΎ π΅)βπ₯) < π} β (π βΎt (π΅ β© dom πΉ)))) |
89 | 30, 88 | mpd 15 |
. 2
β’ ((π β§ π β β) β {π₯ β (π΅ β© dom πΉ) β£ ((πΉ βΎ π΅)βπ₯) < π} β (π βΎt (π΅ β© dom πΉ))) |
90 | 1, 2, 7, 21, 89 | issmfd 45062 |
1
β’ (π β (πΉ βΎ π΅) β (SMblFnβπ)) |