Step | Hyp | Ref
| Expression |
1 | | dfsymdif4 4213 |
. . . . 5
β’ ((β‘(π₯ β π΅ β¦ πΆ) β π¦) β³ (β‘(π₯ β π΅ β¦ π·) β π¦)) = {π§ β£ Β¬ (π§ β (β‘(π₯ β π΅ β¦ πΆ) β π¦) β π§ β (β‘(π₯ β π΅ β¦ π·) β π¦))} |
2 | | eldif 3925 |
. . . . . . . . . . . 12
β’ (π§ β (π΅ β π΄) β (π§ β π΅ β§ Β¬ π§ β π΄)) |
3 | | mbfeqa.3 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = π·) |
4 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π΅ β π΄) β π₯ β π΅) |
5 | | mbfeqalem.4 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β π΅) β πΆ β β) |
6 | 4, 5 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ β β) |
7 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π΅ β¦ πΆ) = (π₯ β π΅ β¦ πΆ) |
8 | 7 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β π΅ β§ πΆ β β) β ((π₯ β π΅ β¦ πΆ)βπ₯) = πΆ) |
9 | 4, 6, 8 | syl2an2 685 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (π΅ β π΄)) β ((π₯ β π΅ β¦ πΆ)βπ₯) = πΆ) |
10 | | mbfeqalem.5 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β π΅) β π· β β) |
11 | 4, 10 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (π΅ β π΄)) β π· β β) |
12 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π΅ β¦ π·) = (π₯ β π΅ β¦ π·) |
13 | 12 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β π΅ β§ π· β β) β ((π₯ β π΅ β¦ π·)βπ₯) = π·) |
14 | 4, 11, 13 | syl2an2 685 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (π΅ β π΄)) β ((π₯ β π΅ β¦ π·)βπ₯) = π·) |
15 | 3, 9, 14 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (π΅ β π΄)) β ((π₯ β π΅ β¦ πΆ)βπ₯) = ((π₯ β π΅ β¦ π·)βπ₯)) |
16 | 15 | ralrimiva 3144 |
. . . . . . . . . . . . . . 15
β’ (π β βπ₯ β (π΅ β π΄)((π₯ β π΅ β¦ πΆ)βπ₯) = ((π₯ β π΅ β¦ π·)βπ₯)) |
17 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π§((π₯ β π΅ β¦ πΆ)βπ₯) = ((π₯ β π΅ β¦ π·)βπ₯) |
18 | | nffvmpt1 6858 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯((π₯ β π΅ β¦ πΆ)βπ§) |
19 | | nffvmpt1 6858 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯((π₯ β π΅ β¦ π·)βπ§) |
20 | 18, 19 | nfeq 2921 |
. . . . . . . . . . . . . . . 16
β’
β²π₯((π₯ β π΅ β¦ πΆ)βπ§) = ((π₯ β π΅ β¦ π·)βπ§) |
21 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β ((π₯ β π΅ β¦ πΆ)βπ₯) = ((π₯ β π΅ β¦ πΆ)βπ§)) |
22 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β ((π₯ β π΅ β¦ π·)βπ₯) = ((π₯ β π΅ β¦ π·)βπ§)) |
23 | 21, 22 | eqeq12d 2753 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π§ β (((π₯ β π΅ β¦ πΆ)βπ₯) = ((π₯ β π΅ β¦ π·)βπ₯) β ((π₯ β π΅ β¦ πΆ)βπ§) = ((π₯ β π΅ β¦ π·)βπ§))) |
24 | 17, 20, 23 | cbvralw 3292 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
(π΅ β π΄)((π₯ β π΅ β¦ πΆ)βπ₯) = ((π₯ β π΅ β¦ π·)βπ₯) β βπ§ β (π΅ β π΄)((π₯ β π΅ β¦ πΆ)βπ§) = ((π₯ β π΅ β¦ π·)βπ§)) |
25 | 16, 24 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β βπ§ β (π΅ β π΄)((π₯ β π΅ β¦ πΆ)βπ§) = ((π₯ β π΅ β¦ π·)βπ§)) |
26 | 25 | r19.21bi 3237 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β (π΅ β π΄)) β ((π₯ β π΅ β¦ πΆ)βπ§) = ((π₯ β π΅ β¦ π·)βπ§)) |
27 | 26 | eleq1d 2823 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (π΅ β π΄)) β (((π₯ β π΅ β¦ πΆ)βπ§) β π¦ β ((π₯ β π΅ β¦ π·)βπ§) β π¦)) |
28 | 2, 27 | sylan2br 596 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π΅ β§ Β¬ π§ β π΄)) β (((π₯ β π΅ β¦ πΆ)βπ§) β π¦ β ((π₯ β π΅ β¦ π·)βπ§) β π¦)) |
29 | 28 | anass1rs 654 |
. . . . . . . . . 10
β’ (((π β§ Β¬ π§ β π΄) β§ π§ β π΅) β (((π₯ β π΅ β¦ πΆ)βπ§) β π¦ β ((π₯ β π΅ β¦ π·)βπ§) β π¦)) |
30 | 29 | pm5.32da 580 |
. . . . . . . . 9
β’ ((π β§ Β¬ π§ β π΄) β ((π§ β π΅ β§ ((π₯ β π΅ β¦ πΆ)βπ§) β π¦) β (π§ β π΅ β§ ((π₯ β π΅ β¦ π·)βπ§) β π¦))) |
31 | 5 | fmpttd 7068 |
. . . . . . . . . . . 12
β’ (π β (π₯ β π΅ β¦ πΆ):π΅βΆβ) |
32 | 31 | ffnd 6674 |
. . . . . . . . . . 11
β’ (π β (π₯ β π΅ β¦ πΆ) Fn π΅) |
33 | 32 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π§ β π΄) β (π₯ β π΅ β¦ πΆ) Fn π΅) |
34 | | elpreima 7013 |
. . . . . . . . . 10
β’ ((π₯ β π΅ β¦ πΆ) Fn π΅ β (π§ β (β‘(π₯ β π΅ β¦ πΆ) β π¦) β (π§ β π΅ β§ ((π₯ β π΅ β¦ πΆ)βπ§) β π¦))) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
β’ ((π β§ Β¬ π§ β π΄) β (π§ β (β‘(π₯ β π΅ β¦ πΆ) β π¦) β (π§ β π΅ β§ ((π₯ β π΅ β¦ πΆ)βπ§) β π¦))) |
36 | 10 | fmpttd 7068 |
. . . . . . . . . . . 12
β’ (π β (π₯ β π΅ β¦ π·):π΅βΆβ) |
37 | 36 | ffnd 6674 |
. . . . . . . . . . 11
β’ (π β (π₯ β π΅ β¦ π·) Fn π΅) |
38 | 37 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π§ β π΄) β (π₯ β π΅ β¦ π·) Fn π΅) |
39 | | elpreima 7013 |
. . . . . . . . . 10
β’ ((π₯ β π΅ β¦ π·) Fn π΅ β (π§ β (β‘(π₯ β π΅ β¦ π·) β π¦) β (π§ β π΅ β§ ((π₯ β π΅ β¦ π·)βπ§) β π¦))) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
β’ ((π β§ Β¬ π§ β π΄) β (π§ β (β‘(π₯ β π΅ β¦ π·) β π¦) β (π§ β π΅ β§ ((π₯ β π΅ β¦ π·)βπ§) β π¦))) |
41 | 30, 35, 40 | 3bitr4d 311 |
. . . . . . . 8
β’ ((π β§ Β¬ π§ β π΄) β (π§ β (β‘(π₯ β π΅ β¦ πΆ) β π¦) β π§ β (β‘(π₯ β π΅ β¦ π·) β π¦))) |
42 | 41 | ex 414 |
. . . . . . 7
β’ (π β (Β¬ π§ β π΄ β (π§ β (β‘(π₯ β π΅ β¦ πΆ) β π¦) β π§ β (β‘(π₯ β π΅ β¦ π·) β π¦)))) |
43 | 42 | con1d 145 |
. . . . . 6
β’ (π β (Β¬ (π§ β (β‘(π₯ β π΅ β¦ πΆ) β π¦) β π§ β (β‘(π₯ β π΅ β¦ π·) β π¦)) β π§ β π΄)) |
44 | 43 | abssdv 4030 |
. . . . 5
β’ (π β {π§ β£ Β¬ (π§ β (β‘(π₯ β π΅ β¦ πΆ) β π¦) β π§ β (β‘(π₯ β π΅ β¦ π·) β π¦))} β π΄) |
45 | 1, 44 | eqsstrid 3997 |
. . . 4
β’ (π β ((β‘(π₯ β π΅ β¦ πΆ) β π¦) β³ (β‘(π₯ β π΅ β¦ π·) β π¦)) β π΄) |
46 | 45 | difsymssdifssd 4218 |
. . 3
β’ (π β ((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦)) β π΄) |
47 | | mbfeqa.1 |
. . 3
β’ (π β π΄ β β) |
48 | 46, 47 | sstrd 3959 |
. 2
β’ (π β ((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦)) β β) |
49 | | mbfeqa.2 |
. . 3
β’ (π β (vol*βπ΄) = 0) |
50 | | ovolssnul 24867 |
. . 3
β’ ((((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦)) β π΄ β§ π΄ β β β§ (vol*βπ΄) = 0) β
(vol*β((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦))) = 0) |
51 | 46, 47, 49, 50 | syl3anc 1372 |
. 2
β’ (π β (vol*β((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦))) = 0) |
52 | | nulmbl 24915 |
. 2
β’ ((((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦)) β β β§ (vol*β((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦))) = 0) β ((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦)) β dom vol) |
53 | 48, 51, 52 | syl2anc 585 |
1
β’ (π β ((β‘(π₯ β π΅ β¦ πΆ) β π¦) β (β‘(π₯ β π΅ β¦ π·) β π¦)) β dom vol) |