Step | Hyp | Ref
| Expression |
1 | | mntoval.1 |
. . . . 5
β’ π΄ = (Baseβπ) |
2 | | mntoval.2 |
. . . . 5
β’ π΅ = (Baseβπ) |
3 | | mntoval.3 |
. . . . 5
β’ β€ =
(leβπ) |
4 | | mntoval.4 |
. . . . 5
β’ β² =
(leβπ) |
5 | 1, 2, 3, 4 | mntoval 31891 |
. . . 4
β’ ((π β π β§ π β π) β (πMonotπ) = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))}) |
6 | 5 | eleq2d 2820 |
. . 3
β’ ((π β π β§ π β π) β (πΉ β (πMonotπ) β πΉ β {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))})) |
7 | | fveq1 6842 |
. . . . . . 7
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
8 | | fveq1 6842 |
. . . . . . 7
β’ (π = πΉ β (πβπ¦) = (πΉβπ¦)) |
9 | 7, 8 | breq12d 5119 |
. . . . . 6
β’ (π = πΉ β ((πβπ₯) β² (πβπ¦) β (πΉβπ₯) β² (πΉβπ¦))) |
10 | 9 | imbi2d 341 |
. . . . 5
β’ (π = πΉ β ((π₯ β€ π¦ β (πβπ₯) β² (πβπ¦)) β (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)))) |
11 | 10 | 2ralbidv 3209 |
. . . 4
β’ (π = πΉ β (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦)) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)))) |
12 | 11 | elrab 3646 |
. . 3
β’ (πΉ β {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))} β (πΉ β (π΅ βm π΄) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)))) |
13 | 6, 12 | bitrdi 287 |
. 2
β’ ((π β π β§ π β π) β (πΉ β (πMonotπ) β (πΉ β (π΅ βm π΄) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))))) |
14 | 2 | fvexi 6857 |
. . . 4
β’ π΅ β V |
15 | 1 | fvexi 6857 |
. . . 4
β’ π΄ β V |
16 | 14, 15 | elmap 8812 |
. . 3
β’ (πΉ β (π΅ βm π΄) β πΉ:π΄βΆπ΅) |
17 | 16 | anbi1i 625 |
. 2
β’ ((πΉ β (π΅ βm π΄) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)))) |
18 | 13, 17 | bitrdi 287 |
1
β’ ((π β π β§ π β π) β (πΉ β (πMonotπ) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))))) |