Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . 4
β’ (((π΄ β dom vol β§ π΅ β β) β§ π₯ β π΄) β π΅ β β) |
2 | | fconstmpt 5699 |
. . . 4
β’ (π΄ Γ {π΅}) = (π₯ β π΄ β¦ π΅) |
3 | 1, 2 | fmptd 7067 |
. . 3
β’ ((π΄ β dom vol β§ π΅ β β) β (π΄ Γ {π΅}):π΄βΆβ) |
4 | | mblss 24911 |
. . . 4
β’ (π΄ β dom vol β π΄ β
β) |
5 | 4 | adantr 482 |
. . 3
β’ ((π΄ β dom vol β§ π΅ β β) β π΄ β
β) |
6 | | cnex 11139 |
. . . 4
β’ β
β V |
7 | | reex 11149 |
. . . 4
β’ β
β V |
8 | | elpm2r 8790 |
. . . 4
β’
(((β β V β§ β β V) β§ ((π΄ Γ {π΅}):π΄βΆβ β§ π΄ β β)) β (π΄ Γ {π΅}) β (β βpm
β)) |
9 | 6, 7, 8 | mpanl12 701 |
. . 3
β’ (((π΄ Γ {π΅}):π΄βΆβ β§ π΄ β β) β (π΄ Γ {π΅}) β (β βpm
β)) |
10 | 3, 5, 9 | syl2anc 585 |
. 2
β’ ((π΄ β dom vol β§ π΅ β β) β (π΄ Γ {π΅}) β (β βpm
β)) |
11 | 2 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β dom vol β§ π΅ β β) β (π΄ Γ {π΅}) = (π₯ β π΄ β¦ π΅)) |
12 | | ref 15004 |
. . . . . . . . . . 11
β’
β:ββΆβ |
13 | 12 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β dom vol β§ π΅ β β) β
β:ββΆβ) |
14 | 13 | feqmptd 6915 |
. . . . . . . . 9
β’ ((π΄ β dom vol β§ π΅ β β) β β =
(π¦ β β β¦
(ββπ¦))) |
15 | | fveq2 6847 |
. . . . . . . . 9
β’ (π¦ = π΅ β (ββπ¦) = (ββπ΅)) |
16 | 1, 11, 14, 15 | fmptco 7080 |
. . . . . . . 8
β’ ((π΄ β dom vol β§ π΅ β β) β (β
β (π΄ Γ {π΅})) = (π₯ β π΄ β¦ (ββπ΅))) |
17 | | fconstmpt 5699 |
. . . . . . . 8
β’ (π΄ Γ {(ββπ΅)}) = (π₯ β π΄ β¦ (ββπ΅)) |
18 | 16, 17 | eqtr4di 2795 |
. . . . . . 7
β’ ((π΄ β dom vol β§ π΅ β β) β (β
β (π΄ Γ {π΅})) = (π΄ Γ {(ββπ΅)})) |
19 | 18 | cnveqd 5836 |
. . . . . 6
β’ ((π΄ β dom vol β§ π΅ β β) β β‘(β β (π΄ Γ {π΅})) = β‘(π΄ Γ {(ββπ΅)})) |
20 | 19 | imaeq1d 6017 |
. . . . 5
β’ ((π΄ β dom vol β§ π΅ β β) β (β‘(β β (π΄ Γ {π΅})) β π¦) = (β‘(π΄ Γ {(ββπ΅)}) β π¦)) |
21 | | recl 15002 |
. . . . . 6
β’ (π΅ β β β
(ββπ΅) β
β) |
22 | | mbfconstlem 25007 |
. . . . . 6
β’ ((π΄ β dom vol β§
(ββπ΅) β
β) β (β‘(π΄ Γ {(ββπ΅)}) β π¦) β dom vol) |
23 | 21, 22 | sylan2 594 |
. . . . 5
β’ ((π΄ β dom vol β§ π΅ β β) β (β‘(π΄ Γ {(ββπ΅)}) β π¦) β dom vol) |
24 | 20, 23 | eqeltrd 2838 |
. . . 4
β’ ((π΄ β dom vol β§ π΅ β β) β (β‘(β β (π΄ Γ {π΅})) β π¦) β dom vol) |
25 | | imf 15005 |
. . . . . . . . . . 11
β’
β:ββΆβ |
26 | 25 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β dom vol β§ π΅ β β) β
β:ββΆβ) |
27 | 26 | feqmptd 6915 |
. . . . . . . . 9
β’ ((π΄ β dom vol β§ π΅ β β) β β
= (π¦ β β β¦
(ββπ¦))) |
28 | | fveq2 6847 |
. . . . . . . . 9
β’ (π¦ = π΅ β (ββπ¦) = (ββπ΅)) |
29 | 1, 11, 27, 28 | fmptco 7080 |
. . . . . . . 8
β’ ((π΄ β dom vol β§ π΅ β β) β (β
β (π΄ Γ {π΅})) = (π₯ β π΄ β¦ (ββπ΅))) |
30 | | fconstmpt 5699 |
. . . . . . . 8
β’ (π΄ Γ {(ββπ΅)}) = (π₯ β π΄ β¦ (ββπ΅)) |
31 | 29, 30 | eqtr4di 2795 |
. . . . . . 7
β’ ((π΄ β dom vol β§ π΅ β β) β (β
β (π΄ Γ {π΅})) = (π΄ Γ {(ββπ΅)})) |
32 | 31 | cnveqd 5836 |
. . . . . 6
β’ ((π΄ β dom vol β§ π΅ β β) β β‘(β β (π΄ Γ {π΅})) = β‘(π΄ Γ {(ββπ΅)})) |
33 | 32 | imaeq1d 6017 |
. . . . 5
β’ ((π΄ β dom vol β§ π΅ β β) β (β‘(β β (π΄ Γ {π΅})) β π¦) = (β‘(π΄ Γ {(ββπ΅)}) β π¦)) |
34 | | imcl 15003 |
. . . . . 6
β’ (π΅ β β β
(ββπ΅) β
β) |
35 | | mbfconstlem 25007 |
. . . . . 6
β’ ((π΄ β dom vol β§
(ββπ΅) β
β) β (β‘(π΄ Γ {(ββπ΅)}) β π¦) β dom vol) |
36 | 34, 35 | sylan2 594 |
. . . . 5
β’ ((π΄ β dom vol β§ π΅ β β) β (β‘(π΄ Γ {(ββπ΅)}) β π¦) β dom vol) |
37 | 33, 36 | eqeltrd 2838 |
. . . 4
β’ ((π΄ β dom vol β§ π΅ β β) β (β‘(β β (π΄ Γ {π΅})) β π¦) β dom vol) |
38 | 24, 37 | jca 513 |
. . 3
β’ ((π΄ β dom vol β§ π΅ β β) β ((β‘(β β (π΄ Γ {π΅})) β π¦) β dom vol β§ (β‘(β β (π΄ Γ {π΅})) β π¦) β dom vol)) |
39 | 38 | ralrimivw 3148 |
. 2
β’ ((π΄ β dom vol β§ π΅ β β) β
βπ¦ β ran
(,)((β‘(β β (π΄ Γ {π΅})) β π¦) β dom vol β§ (β‘(β β (π΄ Γ {π΅})) β π¦) β dom vol)) |
40 | | ismbf1 25004 |
. 2
β’ ((π΄ Γ {π΅}) β MblFn β ((π΄ Γ {π΅}) β (β βpm
β) β§ βπ¦
β ran (,)((β‘(β β (π΄ Γ {π΅})) β π¦) β dom vol β§ (β‘(β β (π΄ Γ {π΅})) β π¦) β dom vol))) |
41 | 10, 39, 40 | sylanbrc 584 |
1
β’ ((π΄ β dom vol β§ π΅ β β) β (π΄ Γ {π΅}) β MblFn) |