Step | Hyp | Ref
| Expression |
1 | | i1fd.1 |
. . . . . . . . 9
β’ (π β πΉ:ββΆβ) |
2 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β πΉ:ββΆβ) |
3 | | ffun 6676 |
. . . . . . . 8
β’ (πΉ:ββΆβ β
Fun πΉ) |
4 | | funcnvcnv 6573 |
. . . . . . . 8
β’ (Fun
πΉ β Fun β‘β‘πΉ) |
5 | | imadif 6590 |
. . . . . . . 8
β’ (Fun
β‘β‘πΉ β (β‘πΉ β (β β (β β
π₯))) = ((β‘πΉ β β) β (β‘πΉ β (β β π₯)))) |
6 | 2, 3, 4, 5 | 4syl 19 |
. . . . . . 7
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β (β‘πΉ β (β β (β β
π₯))) = ((β‘πΉ β β) β (β‘πΉ β (β β π₯)))) |
7 | | ioof 13371 |
. . . . . . . . . . . . 13
β’
(,):(β* Γ β*)βΆπ«
β |
8 | | frn 6680 |
. . . . . . . . . . . . 13
β’
((,):(β* Γ β*)βΆπ«
β β ran (,) β π« β) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ran (,)
β π« β |
10 | 9 | sseli 3945 |
. . . . . . . . . . 11
β’ (π₯ β ran (,) β π₯ β π«
β) |
11 | 10 | elpwid 4574 |
. . . . . . . . . 10
β’ (π₯ β ran (,) β π₯ β
β) |
12 | 11 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β π₯ β β) |
13 | | dfss4 4223 |
. . . . . . . . 9
β’ (π₯ β β β (β
β (β β π₯)) = π₯) |
14 | 12, 13 | sylib 217 |
. . . . . . . 8
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β (β β
(β β π₯)) =
π₯) |
15 | 14 | imaeq2d 6018 |
. . . . . . 7
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β (β‘πΉ β (β β (β β
π₯))) = (β‘πΉ β π₯)) |
16 | 6, 15 | eqtr3d 2779 |
. . . . . 6
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β ((β‘πΉ β β) β (β‘πΉ β (β β π₯))) = (β‘πΉ β π₯)) |
17 | | fimacnv 6695 |
. . . . . . . . 9
β’ (πΉ:ββΆβ β
(β‘πΉ β β) =
β) |
18 | 2, 17 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β (β‘πΉ β β) =
β) |
19 | | rembl 24920 |
. . . . . . . 8
β’ β
β dom vol |
20 | 18, 19 | eqeltrdi 2846 |
. . . . . . 7
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β (β‘πΉ β β) β dom
vol) |
21 | 1 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ 0 β π¦) β πΉ:ββΆβ) |
22 | | inpreima 7019 |
. . . . . . . . . . . . . 14
β’ (Fun
πΉ β (β‘πΉ β (π¦ β© ran πΉ)) = ((β‘πΉ β π¦) β© (β‘πΉ β ran πΉ))) |
23 | | iunid 5025 |
. . . . . . . . . . . . . . . 16
β’ βͺ π₯ β (π¦ β© ran πΉ){π₯} = (π¦ β© ran πΉ) |
24 | 23 | imaeq2i 6016 |
. . . . . . . . . . . . . . 15
β’ (β‘πΉ β βͺ
π₯ β (π¦ β© ran πΉ){π₯}) = (β‘πΉ β (π¦ β© ran πΉ)) |
25 | | imaiun 7197 |
. . . . . . . . . . . . . . 15
β’ (β‘πΉ β βͺ
π₯ β (π¦ β© ran πΉ){π₯}) = βͺ
π₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯}) |
26 | 24, 25 | eqtr3i 2767 |
. . . . . . . . . . . . . 14
β’ (β‘πΉ β (π¦ β© ran πΉ)) = βͺ
π₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯}) |
27 | | cnvimass 6038 |
. . . . . . . . . . . . . . . 16
β’ (β‘πΉ β π¦) β dom πΉ |
28 | | cnvimarndm 6039 |
. . . . . . . . . . . . . . . 16
β’ (β‘πΉ β ran πΉ) = dom πΉ |
29 | 27, 28 | sseqtrri 3986 |
. . . . . . . . . . . . . . 15
β’ (β‘πΉ β π¦) β (β‘πΉ β ran πΉ) |
30 | | df-ss 3932 |
. . . . . . . . . . . . . . 15
β’ ((β‘πΉ β π¦) β (β‘πΉ β ran πΉ) β ((β‘πΉ β π¦) β© (β‘πΉ β ran πΉ)) = (β‘πΉ β π¦)) |
31 | 29, 30 | mpbi 229 |
. . . . . . . . . . . . . 14
β’ ((β‘πΉ β π¦) β© (β‘πΉ β ran πΉ)) = (β‘πΉ β π¦) |
32 | 22, 26, 31 | 3eqtr3g 2800 |
. . . . . . . . . . . . 13
β’ (Fun
πΉ β βͺ π₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯}) = (β‘πΉ β π¦)) |
33 | 21, 3, 32 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ 0 β π¦) β βͺ π₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯}) = (β‘πΉ β π¦)) |
34 | | i1fd.2 |
. . . . . . . . . . . . . . 15
β’ (π β ran πΉ β Fin) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ 0 β π¦) β ran πΉ β Fin) |
36 | | inss2 4194 |
. . . . . . . . . . . . . 14
β’ (π¦ β© ran πΉ) β ran πΉ |
37 | | ssfi 9124 |
. . . . . . . . . . . . . 14
β’ ((ran
πΉ β Fin β§ (π¦ β© ran πΉ) β ran πΉ) β (π¦ β© ran πΉ) β Fin) |
38 | 35, 36, 37 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ 0 β π¦) β (π¦ β© ran πΉ) β Fin) |
39 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ 0 β π¦) β§ π₯ β (π¦ β© ran πΉ)) β π) |
40 | | elinel1 4160 |
. . . . . . . . . . . . . . . . . . . 20
β’ (0 β
(π¦ β© ran πΉ) β 0 β π¦) |
41 | 40 | con3i 154 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬ 0
β π¦ β Β¬ 0
β (π¦ β© ran πΉ)) |
42 | 41 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ 0 β π¦) β Β¬ 0 β (π¦ β© ran πΉ)) |
43 | | disjsn 4677 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β© ran πΉ) β© {0}) = β
β Β¬ 0 β
(π¦ β© ran πΉ)) |
44 | 42, 43 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ 0 β π¦) β ((π¦ β© ran πΉ) β© {0}) = β
) |
45 | | reldisj 4416 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β© ran πΉ) β ran πΉ β (((π¦ β© ran πΉ) β© {0}) = β
β (π¦ β© ran πΉ) β (ran πΉ β {0}))) |
46 | 36, 45 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦ β© ran πΉ) β© {0}) = β
β (π¦ β© ran πΉ) β (ran πΉ β {0})) |
47 | 44, 46 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ 0 β π¦) β (π¦ β© ran πΉ) β (ran πΉ β {0})) |
48 | 47 | sselda 3949 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ 0 β π¦) β§ π₯ β (π¦ β© ran πΉ)) β π₯ β (ran πΉ β {0})) |
49 | | i1fd.3 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (ran πΉ β {0})) β (β‘πΉ β {π₯}) β dom vol) |
50 | 39, 48, 49 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ 0 β π¦) β§ π₯ β (π¦ β© ran πΉ)) β (β‘πΉ β {π₯}) β dom vol) |
51 | 50 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ 0 β π¦) β βπ₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯}) β dom vol) |
52 | | finiunmbl 24924 |
. . . . . . . . . . . . 13
β’ (((π¦ β© ran πΉ) β Fin β§ βπ₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯}) β dom vol) β βͺ π₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯}) β dom vol) |
53 | 38, 51, 52 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ 0 β π¦) β βͺ π₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯}) β dom vol) |
54 | 33, 53 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ 0 β π¦) β (β‘πΉ β π¦) β dom vol) |
55 | 54 | ex 414 |
. . . . . . . . . 10
β’ (π β (Β¬ 0 β π¦ β (β‘πΉ β π¦) β dom vol)) |
56 | 55 | alrimiv 1931 |
. . . . . . . . 9
β’ (π β βπ¦(Β¬ 0 β π¦ β (β‘πΉ β π¦) β dom vol)) |
57 | 56 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β βπ¦(Β¬ 0 β π¦ β (β‘πΉ β π¦) β dom vol)) |
58 | | elndif 4093 |
. . . . . . . . 9
β’ (0 β
π₯ β Β¬ 0 β
(β β π₯)) |
59 | 58 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β Β¬ 0 β (β
β π₯)) |
60 | | reex 11149 |
. . . . . . . . . 10
β’ β
β V |
61 | 60 | difexi 5290 |
. . . . . . . . 9
β’ (β
β π₯) β
V |
62 | | eleq2 2827 |
. . . . . . . . . . 11
β’ (π¦ = (β β π₯) β (0 β π¦ β 0 β (β
β π₯))) |
63 | 62 | notbid 318 |
. . . . . . . . . 10
β’ (π¦ = (β β π₯) β (Β¬ 0 β π¦ β Β¬ 0 β (β
β π₯))) |
64 | | imaeq2 6014 |
. . . . . . . . . . 11
β’ (π¦ = (β β π₯) β (β‘πΉ β π¦) = (β‘πΉ β (β β π₯))) |
65 | 64 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π¦ = (β β π₯) β ((β‘πΉ β π¦) β dom vol β (β‘πΉ β (β β π₯)) β dom vol)) |
66 | 63, 65 | imbi12d 345 |
. . . . . . . . 9
β’ (π¦ = (β β π₯) β ((Β¬ 0 β π¦ β (β‘πΉ β π¦) β dom vol) β (Β¬ 0 β
(β β π₯) β
(β‘πΉ β (β β π₯)) β dom vol))) |
67 | 61, 66 | spcv 3567 |
. . . . . . . 8
β’
(βπ¦(Β¬ 0
β π¦ β (β‘πΉ β π¦) β dom vol) β (Β¬ 0 β
(β β π₯) β
(β‘πΉ β (β β π₯)) β dom vol)) |
68 | 57, 59, 67 | sylc 65 |
. . . . . . 7
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β (β‘πΉ β (β β π₯)) β dom vol) |
69 | | difmbl 24923 |
. . . . . . 7
β’ (((β‘πΉ β β) β dom vol β§
(β‘πΉ β (β β π₯)) β dom vol) β ((β‘πΉ β β) β (β‘πΉ β (β β π₯))) β dom vol) |
70 | 20, 68, 69 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β ((β‘πΉ β β) β (β‘πΉ β (β β π₯))) β dom vol) |
71 | 16, 70 | eqeltrrd 2839 |
. . . . 5
β’ (((π β§ π₯ β ran (,)) β§ 0 β π₯) β (β‘πΉ β π₯) β dom vol) |
72 | | eleq2 2827 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (0 β π¦ β 0 β π₯)) |
73 | 72 | notbid 318 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (Β¬ 0 β π¦ β Β¬ 0 β π₯)) |
74 | | imaeq2 6014 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (β‘πΉ β π¦) = (β‘πΉ β π₯)) |
75 | 74 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π¦ = π₯ β ((β‘πΉ β π¦) β dom vol β (β‘πΉ β π₯) β dom vol)) |
76 | 73, 75 | imbi12d 345 |
. . . . . . . . 9
β’ (π¦ = π₯ β ((Β¬ 0 β π¦ β (β‘πΉ β π¦) β dom vol) β (Β¬ 0 β
π₯ β (β‘πΉ β π₯) β dom vol))) |
77 | 76 | spvv 2001 |
. . . . . . . 8
β’
(βπ¦(Β¬ 0
β π¦ β (β‘πΉ β π¦) β dom vol) β (Β¬ 0 β
π₯ β (β‘πΉ β π₯) β dom vol)) |
78 | 56, 77 | syl 17 |
. . . . . . 7
β’ (π β (Β¬ 0 β π₯ β (β‘πΉ β π₯) β dom vol)) |
79 | 78 | imp 408 |
. . . . . 6
β’ ((π β§ Β¬ 0 β π₯) β (β‘πΉ β π₯) β dom vol) |
80 | 79 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β ran (,)) β§ Β¬ 0 β π₯) β (β‘πΉ β π₯) β dom vol) |
81 | 71, 80 | pm2.61dan 812 |
. . . 4
β’ ((π β§ π₯ β ran (,)) β (β‘πΉ β π₯) β dom vol) |
82 | 81 | ralrimiva 3144 |
. . 3
β’ (π β βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol) |
83 | | ismbf 25008 |
. . . 4
β’ (πΉ:ββΆβ β
(πΉ β MblFn β
βπ₯ β ran
(,)(β‘πΉ β π₯) β dom vol)) |
84 | 1, 83 | syl 17 |
. . 3
β’ (π β (πΉ β MblFn β βπ₯ β ran (,)(β‘πΉ β π₯) β dom vol)) |
85 | 82, 84 | mpbird 257 |
. 2
β’ (π β πΉ β MblFn) |
86 | | mblvol 24910 |
. . . . . . . 8
β’ ((β‘πΉ β π¦) β dom vol β (volβ(β‘πΉ β π¦)) = (vol*β(β‘πΉ β π¦))) |
87 | 54, 86 | syl 17 |
. . . . . . 7
β’ ((π β§ Β¬ 0 β π¦) β (volβ(β‘πΉ β π¦)) = (vol*β(β‘πΉ β π¦))) |
88 | | mblss 24911 |
. . . . . . . . 9
β’ ((β‘πΉ β π¦) β dom vol β (β‘πΉ β π¦) β β) |
89 | 54, 88 | syl 17 |
. . . . . . . 8
β’ ((π β§ Β¬ 0 β π¦) β (β‘πΉ β π¦) β β) |
90 | | mblvol 24910 |
. . . . . . . . . . 11
β’ ((β‘πΉ β {π₯}) β dom vol β (volβ(β‘πΉ β {π₯})) = (vol*β(β‘πΉ β {π₯}))) |
91 | 50, 90 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ Β¬ 0 β π¦) β§ π₯ β (π¦ β© ran πΉ)) β (volβ(β‘πΉ β {π₯})) = (vol*β(β‘πΉ β {π₯}))) |
92 | | i1fd.4 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (ran πΉ β {0})) β (volβ(β‘πΉ β {π₯})) β β) |
93 | 39, 48, 92 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ Β¬ 0 β π¦) β§ π₯ β (π¦ β© ran πΉ)) β (volβ(β‘πΉ β {π₯})) β β) |
94 | 91, 93 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ Β¬ 0 β π¦) β§ π₯ β (π¦ β© ran πΉ)) β (vol*β(β‘πΉ β {π₯})) β β) |
95 | 38, 94 | fsumrecl 15626 |
. . . . . . . 8
β’ ((π β§ Β¬ 0 β π¦) β Ξ£π₯ β (π¦ β© ran πΉ)(vol*β(β‘πΉ β {π₯})) β β) |
96 | 33 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β§ Β¬ 0 β π¦) β (vol*ββͺ π₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯})) = (vol*β(β‘πΉ β π¦))) |
97 | | mblss 24911 |
. . . . . . . . . . . . 13
β’ ((β‘πΉ β {π₯}) β dom vol β (β‘πΉ β {π₯}) β β) |
98 | 50, 97 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ 0 β π¦) β§ π₯ β (π¦ β© ran πΉ)) β (β‘πΉ β {π₯}) β β) |
99 | 98, 94 | jca 513 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ 0 β π¦) β§ π₯ β (π¦ β© ran πΉ)) β ((β‘πΉ β {π₯}) β β β§ (vol*β(β‘πΉ β {π₯})) β β)) |
100 | 99 | ralrimiva 3144 |
. . . . . . . . . 10
β’ ((π β§ Β¬ 0 β π¦) β βπ₯ β (π¦ β© ran πΉ)((β‘πΉ β {π₯}) β β β§ (vol*β(β‘πΉ β {π₯})) β β)) |
101 | | ovolfiniun 24881 |
. . . . . . . . . 10
β’ (((π¦ β© ran πΉ) β Fin β§ βπ₯ β (π¦ β© ran πΉ)((β‘πΉ β {π₯}) β β β§ (vol*β(β‘πΉ β {π₯})) β β)) β
(vol*ββͺ π₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯})) β€ Ξ£π₯ β (π¦ β© ran πΉ)(vol*β(β‘πΉ β {π₯}))) |
102 | 38, 100, 101 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ Β¬ 0 β π¦) β (vol*ββͺ π₯ β (π¦ β© ran πΉ)(β‘πΉ β {π₯})) β€ Ξ£π₯ β (π¦ β© ran πΉ)(vol*β(β‘πΉ β {π₯}))) |
103 | 96, 102 | eqbrtrrd 5134 |
. . . . . . . 8
β’ ((π β§ Β¬ 0 β π¦) β (vol*β(β‘πΉ β π¦)) β€ Ξ£π₯ β (π¦ β© ran πΉ)(vol*β(β‘πΉ β {π₯}))) |
104 | | ovollecl 24863 |
. . . . . . . 8
β’ (((β‘πΉ β π¦) β β β§ Ξ£π₯ β (π¦ β© ran πΉ)(vol*β(β‘πΉ β {π₯})) β β β§ (vol*β(β‘πΉ β π¦)) β€ Ξ£π₯ β (π¦ β© ran πΉ)(vol*β(β‘πΉ β {π₯}))) β (vol*β(β‘πΉ β π¦)) β β) |
105 | 89, 95, 103, 104 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ Β¬ 0 β π¦) β (vol*β(β‘πΉ β π¦)) β β) |
106 | 87, 105 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ Β¬ 0 β π¦) β (volβ(β‘πΉ β π¦)) β β) |
107 | 106 | ex 414 |
. . . . 5
β’ (π β (Β¬ 0 β π¦ β (volβ(β‘πΉ β π¦)) β β)) |
108 | 107 | alrimiv 1931 |
. . . 4
β’ (π β βπ¦(Β¬ 0 β π¦ β (volβ(β‘πΉ β π¦)) β β)) |
109 | | neldifsn 4757 |
. . . 4
β’ Β¬ 0
β (β β {0}) |
110 | 60 | difexi 5290 |
. . . . 5
β’ (β
β {0}) β V |
111 | | eleq2 2827 |
. . . . . . 7
β’ (π¦ = (β β {0}) β
(0 β π¦ β 0 β
(β β {0}))) |
112 | 111 | notbid 318 |
. . . . . 6
β’ (π¦ = (β β {0}) β
(Β¬ 0 β π¦ β
Β¬ 0 β (β β {0}))) |
113 | | imaeq2 6014 |
. . . . . . . 8
β’ (π¦ = (β β {0}) β
(β‘πΉ β π¦) = (β‘πΉ β (β β
{0}))) |
114 | 113 | fveq2d 6851 |
. . . . . . 7
β’ (π¦ = (β β {0}) β
(volβ(β‘πΉ β π¦)) = (volβ(β‘πΉ β (β β
{0})))) |
115 | 114 | eleq1d 2823 |
. . . . . 6
β’ (π¦ = (β β {0}) β
((volβ(β‘πΉ β π¦)) β β β (volβ(β‘πΉ β (β β {0}))) β
β)) |
116 | 112, 115 | imbi12d 345 |
. . . . 5
β’ (π¦ = (β β {0}) β
((Β¬ 0 β π¦ β
(volβ(β‘πΉ β π¦)) β β) β (Β¬ 0 β
(β β {0}) β (volβ(β‘πΉ β (β β {0}))) β
β))) |
117 | 110, 116 | spcv 3567 |
. . . 4
β’
(βπ¦(Β¬ 0
β π¦ β
(volβ(β‘πΉ β π¦)) β β) β (Β¬ 0 β
(β β {0}) β (volβ(β‘πΉ β (β β {0}))) β
β)) |
118 | 108, 109,
117 | mpisyl 21 |
. . 3
β’ (π β (volβ(β‘πΉ β (β β {0}))) β
β) |
119 | 1, 34, 118 | 3jca 1129 |
. 2
β’ (π β (πΉ:ββΆβ β§ ran πΉ β Fin β§
(volβ(β‘πΉ β (β β {0}))) β
β)) |
120 | | isi1f 25054 |
. 2
β’ (πΉ β dom β«1
β (πΉ β MblFn
β§ (πΉ:ββΆβ β§ ran πΉ β Fin β§
(volβ(β‘πΉ β (β β {0}))) β
β))) |
121 | 85, 119, 120 | sylanbrc 584 |
1
β’ (π β πΉ β dom
β«1) |