Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > homaf | Structured version Visualization version GIF version |
Description: Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.) |
Ref | Expression |
---|---|
homarcl.h | β’ π» = (HomaβπΆ) |
homafval.b | β’ π΅ = (BaseβπΆ) |
homafval.c | β’ (π β πΆ β Cat) |
Ref | Expression |
---|---|
homaf | β’ (π β π»:(π΅ Γ π΅)βΆπ« ((π΅ Γ π΅) Γ V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | homarcl.h | . . 3 β’ π» = (HomaβπΆ) | |
2 | homafval.b | . . 3 β’ π΅ = (BaseβπΆ) | |
3 | homafval.c | . . 3 β’ (π β πΆ β Cat) | |
4 | eqid 2736 | . . 3 β’ (Hom βπΆ) = (Hom βπΆ) | |
5 | 1, 2, 3, 4 | homafval 17841 | . 2 β’ (π β π» = (π₯ β (π΅ Γ π΅) β¦ ({π₯} Γ ((Hom βπΆ)βπ₯)))) |
6 | snssi 4755 | . . . . 5 β’ (π₯ β (π΅ Γ π΅) β {π₯} β (π΅ Γ π΅)) | |
7 | 6 | adantl 482 | . . . 4 β’ ((π β§ π₯ β (π΅ Γ π΅)) β {π₯} β (π΅ Γ π΅)) |
8 | ssv 3956 | . . . 4 β’ ((Hom βπΆ)βπ₯) β V | |
9 | xpss12 5635 | . . . 4 β’ (({π₯} β (π΅ Γ π΅) β§ ((Hom βπΆ)βπ₯) β V) β ({π₯} Γ ((Hom βπΆ)βπ₯)) β ((π΅ Γ π΅) Γ V)) | |
10 | 7, 8, 9 | sylancl 586 | . . 3 β’ ((π β§ π₯ β (π΅ Γ π΅)) β ({π₯} Γ ((Hom βπΆ)βπ₯)) β ((π΅ Γ π΅) Γ V)) |
11 | vsnex 5374 | . . . . 5 β’ {π₯} β V | |
12 | fvex 6838 | . . . . 5 β’ ((Hom βπΆ)βπ₯) β V | |
13 | 11, 12 | xpex 7665 | . . . 4 β’ ({π₯} Γ ((Hom βπΆ)βπ₯)) β V |
14 | 13 | elpw 4551 | . . 3 β’ (({π₯} Γ ((Hom βπΆ)βπ₯)) β π« ((π΅ Γ π΅) Γ V) β ({π₯} Γ ((Hom βπΆ)βπ₯)) β ((π΅ Γ π΅) Γ V)) |
15 | 10, 14 | sylibr 233 | . 2 β’ ((π β§ π₯ β (π΅ Γ π΅)) β ({π₯} Γ ((Hom βπΆ)βπ₯)) β π« ((π΅ Γ π΅) Γ V)) |
16 | 5, 15 | fmpt3d 7046 | 1 β’ (π β π»:(π΅ Γ π΅)βΆπ« ((π΅ Γ π΅) Γ V)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 396 = wceq 1540 β wcel 2105 Vcvv 3441 β wss 3898 π« cpw 4547 {csn 4573 Γ cxp 5618 βΆwf 6475 βcfv 6479 Basecbs 17009 Hom chom 17070 Catccat 17470 Homachoma 17835 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5229 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5176 df-id 5518 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486 df-fv 6487 df-homa 17838 |
This theorem is referenced by: homarcl2 17847 homarel 17848 arwhoma 17857 |
Copyright terms: Public domain | W3C validator |