Step | Hyp | Ref
| Expression |
1 | | df-mnt 31889 |
. . 3
β’ Monot =
(π£ β V, π€ β V β¦
β¦(Baseβπ£) / πβ¦{π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))}) |
2 | 1 | a1i 11 |
. 2
β’ ((π β π β§ π β π) β Monot = (π£ β V, π€ β V β¦
β¦(Baseβπ£) / πβ¦{π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))})) |
3 | | fvexd 6858 |
. . . 4
β’ ((π£ = π β§ π€ = π) β (Baseβπ£) β V) |
4 | | fveq2 6843 |
. . . . . 6
β’ (π£ = π β (Baseβπ£) = (Baseβπ)) |
5 | | mntoval.1 |
. . . . . 6
β’ π΄ = (Baseβπ) |
6 | 4, 5 | eqtr4di 2791 |
. . . . 5
β’ (π£ = π β (Baseβπ£) = π΄) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π£ = π β§ π€ = π) β (Baseβπ£) = π΄) |
8 | | simplr 768 |
. . . . . . . 8
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β π€ = π) |
9 | 8 | fveq2d 6847 |
. . . . . . 7
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β (Baseβπ€) = (Baseβπ)) |
10 | | mntoval.2 |
. . . . . . 7
β’ π΅ = (Baseβπ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . 6
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β (Baseβπ€) = π΅) |
12 | | simpr 486 |
. . . . . 6
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β π = π΄) |
13 | 11, 12 | oveq12d 7376 |
. . . . 5
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β ((Baseβπ€) βm π) = (π΅ βm π΄)) |
14 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β π£ = π) |
15 | 14 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β (leβπ£) = (leβπ)) |
16 | | mntoval.3 |
. . . . . . . . . 10
β’ β€ =
(leβπ) |
17 | 15, 16 | eqtr4di 2791 |
. . . . . . . . 9
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β (leβπ£) = β€ ) |
18 | 17 | breqd 5117 |
. . . . . . . 8
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β (π₯(leβπ£)π¦ β π₯ β€ π¦)) |
19 | 8 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β (leβπ€) = (leβπ)) |
20 | | mntoval.4 |
. . . . . . . . . 10
β’ β² =
(leβπ) |
21 | 19, 20 | eqtr4di 2791 |
. . . . . . . . 9
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β (leβπ€) = β² ) |
22 | 21 | breqd 5117 |
. . . . . . . 8
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β ((πβπ₯)(leβπ€)(πβπ¦) β (πβπ₯) β² (πβπ¦))) |
23 | 18, 22 | imbi12d 345 |
. . . . . . 7
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β ((π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦)) β (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦)))) |
24 | 12, 23 | raleqbidv 3318 |
. . . . . 6
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β (βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦)) β βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦)))) |
25 | 12, 24 | raleqbidv 3318 |
. . . . 5
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β (βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦)) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦)))) |
26 | 13, 25 | rabeqbidv 3423 |
. . . 4
β’ (((π£ = π β§ π€ = π) β§ π = π΄) β {π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))} = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))}) |
27 | 3, 7, 26 | csbied2 3896 |
. . 3
β’ ((π£ = π β§ π€ = π) β β¦(Baseβπ£) / πβ¦{π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))} = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))}) |
28 | 27 | adantl 483 |
. 2
β’ (((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β β¦(Baseβπ£) / πβ¦{π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))} = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))}) |
29 | | elex 3462 |
. . 3
β’ (π β π β π β V) |
30 | 29 | adantr 482 |
. 2
β’ ((π β π β§ π β π) β π β V) |
31 | | elex 3462 |
. . 3
β’ (π β π β π β V) |
32 | 31 | adantl 483 |
. 2
β’ ((π β π β§ π β π) β π β V) |
33 | | eqid 2733 |
. . 3
β’ {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))} = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))} |
34 | | ovexd 7393 |
. . 3
β’ ((π β π β§ π β π) β (π΅ βm π΄) β V) |
35 | 33, 34 | rabexd 5291 |
. 2
β’ ((π β π β§ π β π) β {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))} β V) |
36 | 2, 28, 30, 32, 35 | ovmpod 7508 |
1
β’ ((π β π β§ π β π) β (πMonotπ) = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))}) |