Step | Hyp | Ref
| Expression |
1 | | ismntd.5 |
. . 3
β’ (π β π β πΆ) |
2 | | ismntd.6 |
. . 3
β’ (π β π β π·) |
3 | | ismntd.7 |
. . 3
β’ (π β πΉ β (πMonotπ)) |
4 | | ismntd.1 |
. . . . . 6
β’ π΄ = (Baseβπ) |
5 | | ismntd.2 |
. . . . . 6
β’ π΅ = (Baseβπ) |
6 | | ismntd.3 |
. . . . . 6
β’ β€ =
(leβπ) |
7 | | ismntd.4 |
. . . . . 6
β’ β² =
(leβπ) |
8 | 4, 5, 6, 7 | ismnt 31892 |
. . . . 5
β’ ((π β πΆ β§ π β π·) β (πΉ β (πMonotπ) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))))) |
9 | 8 | biimp3a 1470 |
. . . 4
β’ ((π β πΆ β§ π β π· β§ πΉ β (πMonotπ)) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)))) |
10 | 9 | simprd 497 |
. . 3
β’ ((π β πΆ β§ π β π· β§ πΉ β (πMonotπ)) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
11 | 1, 2, 3, 10 | syl3anc 1372 |
. 2
β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) |
12 | | ismntd.10 |
. 2
β’ (π β π β€ π) |
13 | | breq1 5109 |
. . . 4
β’ (π₯ = π β (π₯ β€ π¦ β π β€ π¦)) |
14 | | fveq2 6843 |
. . . . 5
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
15 | 14 | breq1d 5116 |
. . . 4
β’ (π₯ = π β ((πΉβπ₯) β² (πΉβπ¦) β (πΉβπ) β² (πΉβπ¦))) |
16 | 13, 15 | imbi12d 345 |
. . 3
β’ (π₯ = π β ((π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β (π β€ π¦ β (πΉβπ) β² (πΉβπ¦)))) |
17 | | breq2 5110 |
. . . 4
β’ (π¦ = π β (π β€ π¦ β π β€ π)) |
18 | | fveq2 6843 |
. . . . 5
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
19 | 18 | breq2d 5118 |
. . . 4
β’ (π¦ = π β ((πΉβπ) β² (πΉβπ¦) β (πΉβπ) β² (πΉβπ))) |
20 | 17, 19 | imbi12d 345 |
. . 3
β’ (π¦ = π β ((π β€ π¦ β (πΉβπ) β² (πΉβπ¦)) β (π β€ π β (πΉβπ) β² (πΉβπ)))) |
21 | | ismntd.8 |
. . 3
β’ (π β π β π΄) |
22 | | eqidd 2734 |
. . 3
β’ ((π β§ π₯ = π) β π΄ = π΄) |
23 | | ismntd.9 |
. . 3
β’ (π β π β π΄) |
24 | 16, 20, 21, 22, 23 | rspc2vd 3907 |
. 2
β’ (π β (βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β (π β€ π β (πΉβπ) β² (πΉβπ)))) |
25 | 11, 12, 24 | mp2d 49 |
1
β’ (π β (πΉβπ) β² (πΉβπ)) |