Step | Hyp | Ref
| Expression |
1 | | mbfdm 24993 |
. . 3
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
2 | | fdm 6678 |
. . . 4
β’ (πΉ:π΄βΆβ β dom πΉ = π΄) |
3 | 2 | eleq1d 2823 |
. . 3
β’ (πΉ:π΄βΆβ β (dom πΉ β dom vol β π΄ β dom
vol)) |
4 | 1, 3 | imbitrid 243 |
. 2
β’ (πΉ:π΄βΆβ β (πΉ β MblFn β π΄ β dom vol)) |
5 | | mbfdm 24993 |
. . . 4
β’ ((β
β πΉ) β MblFn
β dom (β β πΉ) β dom vol) |
6 | 5 | adantr 482 |
. . 3
β’ (((β
β πΉ) β MblFn
β§ (β β πΉ)
β MblFn) β dom (β β πΉ) β dom vol) |
7 | | ref 14998 |
. . . . . 6
β’
β:ββΆβ |
8 | | fco 6693 |
. . . . . 6
β’
((β:ββΆβ β§ πΉ:π΄βΆβ) β (β β
πΉ):π΄βΆβ) |
9 | 7, 8 | mpan 689 |
. . . . 5
β’ (πΉ:π΄βΆβ β (β β πΉ):π΄βΆβ) |
10 | 9 | fdmd 6680 |
. . . 4
β’ (πΉ:π΄βΆβ β dom (β β
πΉ) = π΄) |
11 | 10 | eleq1d 2823 |
. . 3
β’ (πΉ:π΄βΆβ β (dom (β β
πΉ) β dom vol β
π΄ β dom
vol)) |
12 | 6, 11 | imbitrid 243 |
. 2
β’ (πΉ:π΄βΆβ β (((β β
πΉ) β MblFn β§
(β β πΉ) β
MblFn) β π΄ β dom
vol)) |
13 | | ismbf1 24991 |
. . . 4
β’ (πΉ β MblFn β (πΉ β (β
βpm β) β§ βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol))) |
14 | 9 | adantr 482 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β β
πΉ):π΄βΆβ) |
15 | | ismbf 24995 |
. . . . . . . 8
β’ ((β
β πΉ):π΄βΆβ β ((β
β πΉ) β MblFn
β βπ₯ β ran
(,)(β‘(β β πΉ) β π₯) β dom vol)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β ((β β
πΉ) β MblFn β
βπ₯ β ran
(,)(β‘(β β πΉ) β π₯) β dom vol)) |
17 | | imf 14999 |
. . . . . . . . . 10
β’
β:ββΆβ |
18 | | fco 6693 |
. . . . . . . . . 10
β’
((β:ββΆβ β§ πΉ:π΄βΆβ) β (β β
πΉ):π΄βΆβ) |
19 | 17, 18 | mpan 689 |
. . . . . . . . 9
β’ (πΉ:π΄βΆβ β (β β
πΉ):π΄βΆβ) |
20 | 19 | adantr 482 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (β β
πΉ):π΄βΆβ) |
21 | | ismbf 24995 |
. . . . . . . 8
β’ ((β
β πΉ):π΄βΆβ β ((β
β πΉ) β MblFn
β βπ₯ β ran
(,)(β‘(β β πΉ) β π₯) β dom vol)) |
22 | 20, 21 | syl 17 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β ((β β
πΉ) β MblFn β
βπ₯ β ran
(,)(β‘(β β πΉ) β π₯) β dom vol)) |
23 | 16, 22 | anbi12d 632 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (((β β
πΉ) β MblFn β§
(β β πΉ) β
MblFn) β (βπ₯
β ran (,)(β‘(β β πΉ) β π₯) β dom vol β§ βπ₯ β ran (,)(β‘(β β πΉ) β π₯) β dom vol))) |
24 | | r19.26 3115 |
. . . . . 6
β’
(βπ₯ β
ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol) β (βπ₯ β ran (,)(β‘(β β πΉ) β π₯) β dom vol β§ βπ₯ β ran (,)(β‘(β β πΉ) β π₯) β dom vol)) |
25 | 23, 24 | bitr4di 289 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (((β β
πΉ) β MblFn β§
(β β πΉ) β
MblFn) β βπ₯
β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol))) |
26 | | mblss 24898 |
. . . . . . 7
β’ (π΄ β dom vol β π΄ β
β) |
27 | | cnex 11133 |
. . . . . . . 8
β’ β
β V |
28 | | reex 11143 |
. . . . . . . 8
β’ β
β V |
29 | | elpm2r 8784 |
. . . . . . . 8
β’
(((β β V β§ β β V) β§ (πΉ:π΄βΆβ β§ π΄ β β)) β πΉ β (β βpm
β)) |
30 | 27, 28, 29 | mpanl12 701 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ β (β βpm
β)) |
31 | 26, 30 | sylan2 594 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β πΉ β (β βpm
β)) |
32 | 31 | biantrurd 534 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol) β (πΉ β (β βpm
β) β§ βπ₯
β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol)))) |
33 | 25, 32 | bitrd 279 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (((β β
πΉ) β MblFn β§
(β β πΉ) β
MblFn) β (πΉ β
(β βpm β) β§ βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol)))) |
34 | 13, 33 | bitr4id 290 |
. . 3
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol) β (πΉ β MblFn β ((β β πΉ) β MblFn β§ (β
β πΉ) β
MblFn))) |
35 | 34 | ex 414 |
. 2
β’ (πΉ:π΄βΆβ β (π΄ β dom vol β (πΉ β MblFn β ((β β πΉ) β MblFn β§ (β
β πΉ) β
MblFn)))) |
36 | 4, 12, 35 | pm5.21ndd 381 |
1
β’ (πΉ:π΄βΆβ β (πΉ β MblFn β ((β β πΉ) β MblFn β§ (β
β πΉ) β
MblFn))) |