Step | Hyp | Ref
| Expression |
1 | | mbfmax.3 |
. . . . 5
β’ (π β πΊ:π΄βΆβ) |
2 | 1 | ffvelcdmda 7040 |
. . . 4
β’ ((π β§ π₯ β π΄) β (πΊβπ₯) β β) |
3 | | mbfmax.1 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
4 | 3 | ffvelcdmda 7040 |
. . . 4
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β) |
5 | 2, 4 | ifcld 4537 |
. . 3
β’ ((π β§ π₯ β π΄) β if((πΉβπ₯) β€ (πΊβπ₯), (πΊβπ₯), (πΉβπ₯)) β β) |
6 | | mbfmax.5 |
. . 3
β’ π» = (π₯ β π΄ β¦ if((πΉβπ₯) β€ (πΊβπ₯), (πΊβπ₯), (πΉβπ₯))) |
7 | 5, 6 | fmptd 7067 |
. 2
β’ (π β π»:π΄βΆβ) |
8 | 3 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β β*) β πΉ:π΄βΆβ) |
9 | 8 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (πΉβπ§) β β) |
10 | 9 | rexrd 11212 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (πΉβπ§) β
β*) |
11 | 1 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β β*) β πΊ:π΄βΆβ) |
12 | 11 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (πΊβπ§) β β) |
13 | 12 | rexrd 11212 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (πΊβπ§) β
β*) |
14 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β π¦ β β*) |
15 | | xrmaxle 13109 |
. . . . . . . . . . . 12
β’ (((πΉβπ§) β β* β§ (πΊβπ§) β β* β§ π¦ β β*)
β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β€ π¦ β ((πΉβπ§) β€ π¦ β§ (πΊβπ§) β€ π¦))) |
16 | 10, 13, 14, 15 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β€ π¦ β ((πΉβπ§) β€ π¦ β§ (πΊβπ§) β€ π¦))) |
17 | 16 | notbid 318 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (Β¬ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β€ π¦ β Β¬ ((πΉβπ§) β€ π¦ β§ (πΊβπ§) β€ π¦))) |
18 | | ianor 981 |
. . . . . . . . . 10
β’ (Β¬
((πΉβπ§) β€ π¦ β§ (πΊβπ§) β€ π¦) β (Β¬ (πΉβπ§) β€ π¦ β¨ Β¬ (πΊβπ§) β€ π¦)) |
19 | 17, 18 | bitrdi 287 |
. . . . . . . . 9
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (Β¬ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β€ π¦ β (Β¬ (πΉβπ§) β€ π¦ β¨ Β¬ (πΊβπ§) β€ π¦))) |
20 | | pnfxr 11216 |
. . . . . . . . . . . . 13
β’ +β
β β* |
21 | | elioo2 13312 |
. . . . . . . . . . . . 13
β’ ((π¦ β β*
β§ +β β β*) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β (π¦(,)+β) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < +β))) |
22 | 14, 20, 21 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β (π¦(,)+β) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < +β))) |
23 | | 3anan12 1097 |
. . . . . . . . . . . 12
β’
((if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < +β) β (π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β§ (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < +β))) |
24 | 22, 23 | bitrdi 287 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β (π¦(,)+β) β (π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β§ (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < +β)))) |
25 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
26 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π§ β (πΊβπ₯) = (πΊβπ§)) |
27 | 25, 26 | breq12d 5123 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π§ β ((πΉβπ₯) β€ (πΊβπ₯) β (πΉβπ§) β€ (πΊβπ§))) |
28 | 27, 26, 25 | ifbieq12d 4519 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β if((πΉβπ₯) β€ (πΊβπ₯), (πΊβπ₯), (πΉβπ₯)) = if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§))) |
29 | | fvex 6860 |
. . . . . . . . . . . . . . 15
β’ (πΊβπ§) β V |
30 | | fvex 6860 |
. . . . . . . . . . . . . . 15
β’ (πΉβπ§) β V |
31 | 29, 30 | ifex 4541 |
. . . . . . . . . . . . . 14
β’ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β V |
32 | 28, 6, 31 | fvmpt 6953 |
. . . . . . . . . . . . 13
β’ (π§ β π΄ β (π»βπ§) = if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§))) |
33 | 32 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (π»βπ§) = if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§))) |
34 | 33 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((π»βπ§) β (π¦(,)+β) β if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β (π¦(,)+β))) |
35 | 12, 9 | ifcld 4537 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β) |
36 | | ltpnf 13048 |
. . . . . . . . . . . . 13
β’
(if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < +β) |
37 | 35, 36 | jccir 523 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < +β)) |
38 | 37 | biantrud 533 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β (π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β§ (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < +β)))) |
39 | 24, 34, 38 | 3bitr4d 311 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((π»βπ§) β (π¦(,)+β) β π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)))) |
40 | 35 | rexrd 11212 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β
β*) |
41 | | xrltnle 11229 |
. . . . . . . . . . 11
β’ ((π¦ β β*
β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β*) β (π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β Β¬ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β€ π¦)) |
42 | 14, 40, 41 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (π¦ < if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β Β¬ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β€ π¦)) |
43 | 39, 42 | bitrd 279 |
. . . . . . . . 9
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((π»βπ§) β (π¦(,)+β) β Β¬ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β€ π¦)) |
44 | | elioo2 13312 |
. . . . . . . . . . . . 13
β’ ((π¦ β β*
β§ +β β β*) β ((πΉβπ§) β (π¦(,)+β) β ((πΉβπ§) β β β§ π¦ < (πΉβπ§) β§ (πΉβπ§) < +β))) |
45 | 14, 20, 44 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΉβπ§) β (π¦(,)+β) β ((πΉβπ§) β β β§ π¦ < (πΉβπ§) β§ (πΉβπ§) < +β))) |
46 | | 3anan12 1097 |
. . . . . . . . . . . 12
β’ (((πΉβπ§) β β β§ π¦ < (πΉβπ§) β§ (πΉβπ§) < +β) β (π¦ < (πΉβπ§) β§ ((πΉβπ§) β β β§ (πΉβπ§) < +β))) |
47 | 45, 46 | bitrdi 287 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΉβπ§) β (π¦(,)+β) β (π¦ < (πΉβπ§) β§ ((πΉβπ§) β β β§ (πΉβπ§) < +β)))) |
48 | | ltpnf 13048 |
. . . . . . . . . . . . 13
β’ ((πΉβπ§) β β β (πΉβπ§) < +β) |
49 | 9, 48 | jccir 523 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΉβπ§) β β β§ (πΉβπ§) < +β)) |
50 | 49 | biantrud 533 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (π¦ < (πΉβπ§) β (π¦ < (πΉβπ§) β§ ((πΉβπ§) β β β§ (πΉβπ§) < +β)))) |
51 | | xrltnle 11229 |
. . . . . . . . . . . 12
β’ ((π¦ β β*
β§ (πΉβπ§) β β*)
β (π¦ < (πΉβπ§) β Β¬ (πΉβπ§) β€ π¦)) |
52 | 14, 10, 51 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (π¦ < (πΉβπ§) β Β¬ (πΉβπ§) β€ π¦)) |
53 | 47, 50, 52 | 3bitr2d 307 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΉβπ§) β (π¦(,)+β) β Β¬ (πΉβπ§) β€ π¦)) |
54 | | elioo2 13312 |
. . . . . . . . . . . . 13
β’ ((π¦ β β*
β§ +β β β*) β ((πΊβπ§) β (π¦(,)+β) β ((πΊβπ§) β β β§ π¦ < (πΊβπ§) β§ (πΊβπ§) < +β))) |
55 | 14, 20, 54 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΊβπ§) β (π¦(,)+β) β ((πΊβπ§) β β β§ π¦ < (πΊβπ§) β§ (πΊβπ§) < +β))) |
56 | | 3anan12 1097 |
. . . . . . . . . . . 12
β’ (((πΊβπ§) β β β§ π¦ < (πΊβπ§) β§ (πΊβπ§) < +β) β (π¦ < (πΊβπ§) β§ ((πΊβπ§) β β β§ (πΊβπ§) < +β))) |
57 | 55, 56 | bitrdi 287 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΊβπ§) β (π¦(,)+β) β (π¦ < (πΊβπ§) β§ ((πΊβπ§) β β β§ (πΊβπ§) < +β)))) |
58 | | ltpnf 13048 |
. . . . . . . . . . . . 13
β’ ((πΊβπ§) β β β (πΊβπ§) < +β) |
59 | 12, 58 | jccir 523 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΊβπ§) β β β§ (πΊβπ§) < +β)) |
60 | 59 | biantrud 533 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (π¦ < (πΊβπ§) β (π¦ < (πΊβπ§) β§ ((πΊβπ§) β β β§ (πΊβπ§) < +β)))) |
61 | | xrltnle 11229 |
. . . . . . . . . . . 12
β’ ((π¦ β β*
β§ (πΊβπ§) β β*)
β (π¦ < (πΊβπ§) β Β¬ (πΊβπ§) β€ π¦)) |
62 | 14, 13, 61 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (π¦ < (πΊβπ§) β Β¬ (πΊβπ§) β€ π¦)) |
63 | 57, 60, 62 | 3bitr2d 307 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΊβπ§) β (π¦(,)+β) β Β¬ (πΊβπ§) β€ π¦)) |
64 | 53, 63 | orbi12d 918 |
. . . . . . . . 9
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (((πΉβπ§) β (π¦(,)+β) β¨ (πΊβπ§) β (π¦(,)+β)) β (Β¬ (πΉβπ§) β€ π¦ β¨ Β¬ (πΊβπ§) β€ π¦))) |
65 | 19, 43, 64 | 3bitr4d 311 |
. . . . . . . 8
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((π»βπ§) β (π¦(,)+β) β ((πΉβπ§) β (π¦(,)+β) β¨ (πΊβπ§) β (π¦(,)+β)))) |
66 | 65 | pm5.32da 580 |
. . . . . . 7
β’ ((π β§ π¦ β β*) β ((π§ β π΄ β§ (π»βπ§) β (π¦(,)+β)) β (π§ β π΄ β§ ((πΉβπ§) β (π¦(,)+β) β¨ (πΊβπ§) β (π¦(,)+β))))) |
67 | | andi 1007 |
. . . . . . 7
β’ ((π§ β π΄ β§ ((πΉβπ§) β (π¦(,)+β) β¨ (πΊβπ§) β (π¦(,)+β))) β ((π§ β π΄ β§ (πΉβπ§) β (π¦(,)+β)) β¨ (π§ β π΄ β§ (πΊβπ§) β (π¦(,)+β)))) |
68 | 66, 67 | bitrdi 287 |
. . . . . 6
β’ ((π β§ π¦ β β*) β ((π§ β π΄ β§ (π»βπ§) β (π¦(,)+β)) β ((π§ β π΄ β§ (πΉβπ§) β (π¦(,)+β)) β¨ (π§ β π΄ β§ (πΊβπ§) β (π¦(,)+β))))) |
69 | 7 | ffnd 6674 |
. . . . . . . 8
β’ (π β π» Fn π΄) |
70 | 69 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β β*) β π» Fn π΄) |
71 | | elpreima 7013 |
. . . . . . 7
β’ (π» Fn π΄ β (π§ β (β‘π» β (π¦(,)+β)) β (π§ β π΄ β§ (π»βπ§) β (π¦(,)+β)))) |
72 | 70, 71 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β β*) β (π§ β (β‘π» β (π¦(,)+β)) β (π§ β π΄ β§ (π»βπ§) β (π¦(,)+β)))) |
73 | 8 | ffnd 6674 |
. . . . . . . 8
β’ ((π β§ π¦ β β*) β πΉ Fn π΄) |
74 | | elpreima 7013 |
. . . . . . . 8
β’ (πΉ Fn π΄ β (π§ β (β‘πΉ β (π¦(,)+β)) β (π§ β π΄ β§ (πΉβπ§) β (π¦(,)+β)))) |
75 | 73, 74 | syl 17 |
. . . . . . 7
β’ ((π β§ π¦ β β*) β (π§ β (β‘πΉ β (π¦(,)+β)) β (π§ β π΄ β§ (πΉβπ§) β (π¦(,)+β)))) |
76 | 11 | ffnd 6674 |
. . . . . . . 8
β’ ((π β§ π¦ β β*) β πΊ Fn π΄) |
77 | | elpreima 7013 |
. . . . . . . 8
β’ (πΊ Fn π΄ β (π§ β (β‘πΊ β (π¦(,)+β)) β (π§ β π΄ β§ (πΊβπ§) β (π¦(,)+β)))) |
78 | 76, 77 | syl 17 |
. . . . . . 7
β’ ((π β§ π¦ β β*) β (π§ β (β‘πΊ β (π¦(,)+β)) β (π§ β π΄ β§ (πΊβπ§) β (π¦(,)+β)))) |
79 | 75, 78 | orbi12d 918 |
. . . . . 6
β’ ((π β§ π¦ β β*) β ((π§ β (β‘πΉ β (π¦(,)+β)) β¨ π§ β (β‘πΊ β (π¦(,)+β))) β ((π§ β π΄ β§ (πΉβπ§) β (π¦(,)+β)) β¨ (π§ β π΄ β§ (πΊβπ§) β (π¦(,)+β))))) |
80 | 68, 72, 79 | 3bitr4d 311 |
. . . . 5
β’ ((π β§ π¦ β β*) β (π§ β (β‘π» β (π¦(,)+β)) β (π§ β (β‘πΉ β (π¦(,)+β)) β¨ π§ β (β‘πΊ β (π¦(,)+β))))) |
81 | | elun 4113 |
. . . . 5
β’ (π§ β ((β‘πΉ β (π¦(,)+β)) βͺ (β‘πΊ β (π¦(,)+β))) β (π§ β (β‘πΉ β (π¦(,)+β)) β¨ π§ β (β‘πΊ β (π¦(,)+β)))) |
82 | 80, 81 | bitr4di 289 |
. . . 4
β’ ((π β§ π¦ β β*) β (π§ β (β‘π» β (π¦(,)+β)) β π§ β ((β‘πΉ β (π¦(,)+β)) βͺ (β‘πΊ β (π¦(,)+β))))) |
83 | 82 | eqrdv 2735 |
. . 3
β’ ((π β§ π¦ β β*) β (β‘π» β (π¦(,)+β)) = ((β‘πΉ β (π¦(,)+β)) βͺ (β‘πΊ β (π¦(,)+β)))) |
84 | | mbfmax.2 |
. . . . . 6
β’ (π β πΉ β MblFn) |
85 | | mbfima 25010 |
. . . . . 6
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (π¦(,)+β)) β dom
vol) |
86 | 84, 3, 85 | syl2anc 585 |
. . . . 5
β’ (π β (β‘πΉ β (π¦(,)+β)) β dom
vol) |
87 | | mbfmax.4 |
. . . . . 6
β’ (π β πΊ β MblFn) |
88 | | mbfima 25010 |
. . . . . 6
β’ ((πΊ β MblFn β§ πΊ:π΄βΆβ) β (β‘πΊ β (π¦(,)+β)) β dom
vol) |
89 | 87, 1, 88 | syl2anc 585 |
. . . . 5
β’ (π β (β‘πΊ β (π¦(,)+β)) β dom
vol) |
90 | | unmbl 24917 |
. . . . 5
β’ (((β‘πΉ β (π¦(,)+β)) β dom vol β§ (β‘πΊ β (π¦(,)+β)) β dom vol) β ((β‘πΉ β (π¦(,)+β)) βͺ (β‘πΊ β (π¦(,)+β))) β dom
vol) |
91 | 86, 89, 90 | syl2anc 585 |
. . . 4
β’ (π β ((β‘πΉ β (π¦(,)+β)) βͺ (β‘πΊ β (π¦(,)+β))) β dom
vol) |
92 | 91 | adantr 482 |
. . 3
β’ ((π β§ π¦ β β*) β ((β‘πΉ β (π¦(,)+β)) βͺ (β‘πΊ β (π¦(,)+β))) β dom
vol) |
93 | 83, 92 | eqeltrd 2838 |
. 2
β’ ((π β§ π¦ β β*) β (β‘π» β (π¦(,)+β)) β dom
vol) |
94 | | xrmaxlt 13107 |
. . . . . . . . . 10
β’ (((πΉβπ§) β β* β§ (πΊβπ§) β β* β§ π¦ β β*)
β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦ β ((πΉβπ§) < π¦ β§ (πΊβπ§) < π¦))) |
95 | 10, 13, 14, 94 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦ β ((πΉβπ§) < π¦ β§ (πΊβπ§) < π¦))) |
96 | | mnfxr 11219 |
. . . . . . . . . . . 12
β’ -β
β β* |
97 | | elioo2 13312 |
. . . . . . . . . . . 12
β’
((-β β β* β§ π¦ β β*) β
(if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β (-β(,)π¦) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ -β <
if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦))) |
98 | 96, 14, 97 | sylancr 588 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β (-β(,)π¦) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ -β <
if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦))) |
99 | | df-3an 1090 |
. . . . . . . . . . 11
β’
((if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ -β <
if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦) β ((if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ -β <
if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§))) β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦)) |
100 | 98, 99 | bitrdi 287 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β (-β(,)π¦) β ((if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ -β <
if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§))) β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦))) |
101 | 33 | eleq1d 2823 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((π»βπ§) β (-β(,)π¦) β if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β (-β(,)π¦))) |
102 | | mnflt 13051 |
. . . . . . . . . . . 12
β’
(if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β -β <
if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§))) |
103 | 35, 102 | jccir 523 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ -β <
if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)))) |
104 | 103 | biantrurd 534 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦ β ((if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) β β β§ -β <
if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§))) β§ if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦))) |
105 | 100, 101,
104 | 3bitr4d 311 |
. . . . . . . . 9
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((π»βπ§) β (-β(,)π¦) β if((πΉβπ§) β€ (πΊβπ§), (πΊβπ§), (πΉβπ§)) < π¦)) |
106 | | mnflt 13051 |
. . . . . . . . . . . 12
β’ ((πΉβπ§) β β β -β < (πΉβπ§)) |
107 | 9, 106 | jccir 523 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΉβπ§) β β β§ -β < (πΉβπ§))) |
108 | | elioo2 13312 |
. . . . . . . . . . . . 13
β’
((-β β β* β§ π¦ β β*) β ((πΉβπ§) β (-β(,)π¦) β ((πΉβπ§) β β β§ -β < (πΉβπ§) β§ (πΉβπ§) < π¦))) |
109 | 96, 14, 108 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΉβπ§) β (-β(,)π¦) β ((πΉβπ§) β β β§ -β < (πΉβπ§) β§ (πΉβπ§) < π¦))) |
110 | | df-3an 1090 |
. . . . . . . . . . . 12
β’ (((πΉβπ§) β β β§ -β < (πΉβπ§) β§ (πΉβπ§) < π¦) β (((πΉβπ§) β β β§ -β < (πΉβπ§)) β§ (πΉβπ§) < π¦)) |
111 | 109, 110 | bitrdi 287 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΉβπ§) β (-β(,)π¦) β (((πΉβπ§) β β β§ -β < (πΉβπ§)) β§ (πΉβπ§) < π¦))) |
112 | 107, 111 | mpbirand 706 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΉβπ§) β (-β(,)π¦) β (πΉβπ§) < π¦)) |
113 | | mnflt 13051 |
. . . . . . . . . . . 12
β’ ((πΊβπ§) β β β -β < (πΊβπ§)) |
114 | 12, 113 | jccir 523 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΊβπ§) β β β§ -β < (πΊβπ§))) |
115 | | elioo2 13312 |
. . . . . . . . . . . . 13
β’
((-β β β* β§ π¦ β β*) β ((πΊβπ§) β (-β(,)π¦) β ((πΊβπ§) β β β§ -β < (πΊβπ§) β§ (πΊβπ§) < π¦))) |
116 | 96, 14, 115 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΊβπ§) β (-β(,)π¦) β ((πΊβπ§) β β β§ -β < (πΊβπ§) β§ (πΊβπ§) < π¦))) |
117 | | df-3an 1090 |
. . . . . . . . . . . 12
β’ (((πΊβπ§) β β β§ -β < (πΊβπ§) β§ (πΊβπ§) < π¦) β (((πΊβπ§) β β β§ -β < (πΊβπ§)) β§ (πΊβπ§) < π¦)) |
118 | 116, 117 | bitrdi 287 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΊβπ§) β (-β(,)π¦) β (((πΊβπ§) β β β§ -β < (πΊβπ§)) β§ (πΊβπ§) < π¦))) |
119 | 114, 118 | mpbirand 706 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((πΊβπ§) β (-β(,)π¦) β (πΊβπ§) < π¦)) |
120 | 112, 119 | anbi12d 632 |
. . . . . . . . 9
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β (((πΉβπ§) β (-β(,)π¦) β§ (πΊβπ§) β (-β(,)π¦)) β ((πΉβπ§) < π¦ β§ (πΊβπ§) < π¦))) |
121 | 95, 105, 120 | 3bitr4d 311 |
. . . . . . . 8
β’ (((π β§ π¦ β β*) β§ π§ β π΄) β ((π»βπ§) β (-β(,)π¦) β ((πΉβπ§) β (-β(,)π¦) β§ (πΊβπ§) β (-β(,)π¦)))) |
122 | 121 | pm5.32da 580 |
. . . . . . 7
β’ ((π β§ π¦ β β*) β ((π§ β π΄ β§ (π»βπ§) β (-β(,)π¦)) β (π§ β π΄ β§ ((πΉβπ§) β (-β(,)π¦) β§ (πΊβπ§) β (-β(,)π¦))))) |
123 | | anandi 675 |
. . . . . . 7
β’ ((π§ β π΄ β§ ((πΉβπ§) β (-β(,)π¦) β§ (πΊβπ§) β (-β(,)π¦))) β ((π§ β π΄ β§ (πΉβπ§) β (-β(,)π¦)) β§ (π§ β π΄ β§ (πΊβπ§) β (-β(,)π¦)))) |
124 | 122, 123 | bitrdi 287 |
. . . . . 6
β’ ((π β§ π¦ β β*) β ((π§ β π΄ β§ (π»βπ§) β (-β(,)π¦)) β ((π§ β π΄ β§ (πΉβπ§) β (-β(,)π¦)) β§ (π§ β π΄ β§ (πΊβπ§) β (-β(,)π¦))))) |
125 | | elpreima 7013 |
. . . . . . 7
β’ (π» Fn π΄ β (π§ β (β‘π» β (-β(,)π¦)) β (π§ β π΄ β§ (π»βπ§) β (-β(,)π¦)))) |
126 | 70, 125 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β β*) β (π§ β (β‘π» β (-β(,)π¦)) β (π§ β π΄ β§ (π»βπ§) β (-β(,)π¦)))) |
127 | | elpreima 7013 |
. . . . . . . 8
β’ (πΉ Fn π΄ β (π§ β (β‘πΉ β (-β(,)π¦)) β (π§ β π΄ β§ (πΉβπ§) β (-β(,)π¦)))) |
128 | 73, 127 | syl 17 |
. . . . . . 7
β’ ((π β§ π¦ β β*) β (π§ β (β‘πΉ β (-β(,)π¦)) β (π§ β π΄ β§ (πΉβπ§) β (-β(,)π¦)))) |
129 | | elpreima 7013 |
. . . . . . . 8
β’ (πΊ Fn π΄ β (π§ β (β‘πΊ β (-β(,)π¦)) β (π§ β π΄ β§ (πΊβπ§) β (-β(,)π¦)))) |
130 | 76, 129 | syl 17 |
. . . . . . 7
β’ ((π β§ π¦ β β*) β (π§ β (β‘πΊ β (-β(,)π¦)) β (π§ β π΄ β§ (πΊβπ§) β (-β(,)π¦)))) |
131 | 128, 130 | anbi12d 632 |
. . . . . 6
β’ ((π β§ π¦ β β*) β ((π§ β (β‘πΉ β (-β(,)π¦)) β§ π§ β (β‘πΊ β (-β(,)π¦))) β ((π§ β π΄ β§ (πΉβπ§) β (-β(,)π¦)) β§ (π§ β π΄ β§ (πΊβπ§) β (-β(,)π¦))))) |
132 | 124, 126,
131 | 3bitr4d 311 |
. . . . 5
β’ ((π β§ π¦ β β*) β (π§ β (β‘π» β (-β(,)π¦)) β (π§ β (β‘πΉ β (-β(,)π¦)) β§ π§ β (β‘πΊ β (-β(,)π¦))))) |
133 | | elin 3931 |
. . . . 5
β’ (π§ β ((β‘πΉ β (-β(,)π¦)) β© (β‘πΊ β (-β(,)π¦))) β (π§ β (β‘πΉ β (-β(,)π¦)) β§ π§ β (β‘πΊ β (-β(,)π¦)))) |
134 | 132, 133 | bitr4di 289 |
. . . 4
β’ ((π β§ π¦ β β*) β (π§ β (β‘π» β (-β(,)π¦)) β π§ β ((β‘πΉ β (-β(,)π¦)) β© (β‘πΊ β (-β(,)π¦))))) |
135 | 134 | eqrdv 2735 |
. . 3
β’ ((π β§ π¦ β β*) β (β‘π» β (-β(,)π¦)) = ((β‘πΉ β (-β(,)π¦)) β© (β‘πΊ β (-β(,)π¦)))) |
136 | | mbfima 25010 |
. . . . . 6
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (-β(,)π¦)) β dom vol) |
137 | 84, 3, 136 | syl2anc 585 |
. . . . 5
β’ (π β (β‘πΉ β (-β(,)π¦)) β dom vol) |
138 | | mbfima 25010 |
. . . . . 6
β’ ((πΊ β MblFn β§ πΊ:π΄βΆβ) β (β‘πΊ β (-β(,)π¦)) β dom vol) |
139 | 87, 1, 138 | syl2anc 585 |
. . . . 5
β’ (π β (β‘πΊ β (-β(,)π¦)) β dom vol) |
140 | | inmbl 24922 |
. . . . 5
β’ (((β‘πΉ β (-β(,)π¦)) β dom vol β§ (β‘πΊ β (-β(,)π¦)) β dom vol) β ((β‘πΉ β (-β(,)π¦)) β© (β‘πΊ β (-β(,)π¦))) β dom vol) |
141 | 137, 139,
140 | syl2anc 585 |
. . . 4
β’ (π β ((β‘πΉ β (-β(,)π¦)) β© (β‘πΊ β (-β(,)π¦))) β dom vol) |
142 | 141 | adantr 482 |
. . 3
β’ ((π β§ π¦ β β*) β ((β‘πΉ β (-β(,)π¦)) β© (β‘πΊ β (-β(,)π¦))) β dom vol) |
143 | 135, 142 | eqeltrd 2838 |
. 2
β’ ((π β§ π¦ β β*) β (β‘π» β (-β(,)π¦)) β dom vol) |
144 | 7, 93, 143 | ismbfd 25019 |
1
β’ (π β π» β MblFn) |