Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > yonpropd | Structured version Visualization version GIF version |
Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same Yoneda functor. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Ref | Expression |
---|---|
hofpropd.1 | ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) |
hofpropd.2 | ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) |
hofpropd.c | ⊢ (𝜑 → 𝐶 ∈ Cat) |
hofpropd.d | ⊢ (𝜑 → 𝐷 ∈ Cat) |
Ref | Expression |
---|---|
yonpropd | ⊢ (𝜑 → (Yon‘𝐶) = (Yon‘𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hofpropd.1 | . . . 4 ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) | |
2 | hofpropd.2 | . . . 4 ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) | |
3 | 1 | oppchomfpropd 17482 | . . . 4 ⊢ (𝜑 → (Homf ‘(oppCat‘𝐶)) = (Homf ‘(oppCat‘𝐷))) |
4 | 1, 2 | oppccomfpropd 17483 | . . . 4 ⊢ (𝜑 → (compf‘(oppCat‘𝐶)) = (compf‘(oppCat‘𝐷))) |
5 | hofpropd.c | . . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat) | |
6 | hofpropd.d | . . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat) | |
7 | eqid 2736 | . . . . . 6 ⊢ (oppCat‘𝐶) = (oppCat‘𝐶) | |
8 | 7 | oppccat 17478 | . . . . 5 ⊢ (𝐶 ∈ Cat → (oppCat‘𝐶) ∈ Cat) |
9 | 5, 8 | syl 17 | . . . 4 ⊢ (𝜑 → (oppCat‘𝐶) ∈ Cat) |
10 | eqid 2736 | . . . . . 6 ⊢ (oppCat‘𝐷) = (oppCat‘𝐷) | |
11 | 10 | oppccat 17478 | . . . . 5 ⊢ (𝐷 ∈ Cat → (oppCat‘𝐷) ∈ Cat) |
12 | 6, 11 | syl 17 | . . . 4 ⊢ (𝜑 → (oppCat‘𝐷) ∈ Cat) |
13 | eqid 2736 | . . . . 5 ⊢ (HomF‘(oppCat‘𝐶)) = (HomF‘(oppCat‘𝐶)) | |
14 | eqid 2736 | . . . . 5 ⊢ (SetCat‘ran (Homf ‘𝐶)) = (SetCat‘ran (Homf ‘𝐶)) | |
15 | fvex 6817 | . . . . . . 7 ⊢ (Homf ‘𝐶) ∈ V | |
16 | 15 | rnex 7791 | . . . . . 6 ⊢ ran (Homf ‘𝐶) ∈ V |
17 | 16 | a1i 11 | . . . . 5 ⊢ (𝜑 → ran (Homf ‘𝐶) ∈ V) |
18 | ssidd 3949 | . . . . 5 ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ ran (Homf ‘𝐶)) | |
19 | 7, 13, 14, 5, 17, 18 | oppchofcl 18023 | . . . 4 ⊢ (𝜑 → (HomF‘(oppCat‘𝐶)) ∈ ((𝐶 ×c (oppCat‘𝐶)) Func (SetCat‘ran (Homf ‘𝐶)))) |
20 | 1, 2, 3, 4, 5, 6, 9, 12, 19 | curfpropd 17996 | . . 3 ⊢ (𝜑 → (⟨𝐶, (oppCat‘𝐶)⟩ curryF (HomF‘(oppCat‘𝐶))) = (⟨𝐷, (oppCat‘𝐷)⟩ curryF (HomF‘(oppCat‘𝐶)))) |
21 | 3, 4, 9, 12 | hofpropd 18030 | . . . 4 ⊢ (𝜑 → (HomF‘(oppCat‘𝐶)) = (HomF‘(oppCat‘𝐷))) |
22 | 21 | oveq2d 7323 | . . 3 ⊢ (𝜑 → (⟨𝐷, (oppCat‘𝐷)⟩ curryF (HomF‘(oppCat‘𝐶))) = (⟨𝐷, (oppCat‘𝐷)⟩ curryF (HomF‘(oppCat‘𝐷)))) |
23 | 20, 22 | eqtrd 2776 | . 2 ⊢ (𝜑 → (⟨𝐶, (oppCat‘𝐶)⟩ curryF (HomF‘(oppCat‘𝐶))) = (⟨𝐷, (oppCat‘𝐷)⟩ curryF (HomF‘(oppCat‘𝐷)))) |
24 | eqid 2736 | . . 3 ⊢ (Yon‘𝐶) = (Yon‘𝐶) | |
25 | 24, 5, 7, 13 | yonval 18024 | . 2 ⊢ (𝜑 → (Yon‘𝐶) = (⟨𝐶, (oppCat‘𝐶)⟩ curryF (HomF‘(oppCat‘𝐶)))) |
26 | eqid 2736 | . . 3 ⊢ (Yon‘𝐷) = (Yon‘𝐷) | |
27 | eqid 2736 | . . 3 ⊢ (HomF‘(oppCat‘𝐷)) = (HomF‘(oppCat‘𝐷)) | |
28 | 26, 6, 10, 27 | yonval 18024 | . 2 ⊢ (𝜑 → (Yon‘𝐷) = (⟨𝐷, (oppCat‘𝐷)⟩ curryF (HomF‘(oppCat‘𝐷)))) |
29 | 23, 25, 28 | 3eqtr4d 2786 | 1 ⊢ (𝜑 → (Yon‘𝐶) = (Yon‘𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2104 Vcvv 3437 ⟨cop 4571 ran crn 5601 ‘cfv 6458 (class class class)co 7307 Catccat 17418 Homf chomf 17420 compfccomf 17421 oppCatcoppc 17465 SetCatcsetc 17835 curryF ccurf 17973 HomFchof 18011 Yoncyon 18012 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-rep 5218 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620 ax-cnex 10973 ax-resscn 10974 ax-1cn 10975 ax-icn 10976 ax-addcl 10977 ax-addrcl 10978 ax-mulcl 10979 ax-mulrcl 10980 ax-mulcom 10981 ax-addass 10982 ax-mulass 10983 ax-distr 10984 ax-i2m1 10985 ax-1ne0 10986 ax-1rid 10987 ax-rnegex 10988 ax-rrecex 10989 ax-cnre 10990 ax-pre-lttri 10991 ax-pre-lttrn 10992 ax-pre-ltadd 10993 ax-pre-mulgt0 10994 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3285 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-tp 4570 df-op 4572 df-uni 4845 df-iun 4933 df-br 5082 df-opab 5144 df-mpt 5165 df-tr 5199 df-id 5500 df-eprel 5506 df-po 5514 df-so 5515 df-fr 5555 df-we 5557 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-pred 6217 df-ord 6284 df-on 6285 df-lim 6286 df-suc 6287 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-riota 7264 df-ov 7310 df-oprab 7311 df-mpo 7312 df-om 7745 df-1st 7863 df-2nd 7864 df-tpos 8073 df-frecs 8128 df-wrecs 8159 df-recs 8233 df-rdg 8272 df-1o 8328 df-er 8529 df-map 8648 df-ixp 8717 df-en 8765 df-dom 8766 df-sdom 8767 df-fin 8768 df-pnf 11057 df-mnf 11058 df-xr 11059 df-ltxr 11060 df-le 11061 df-sub 11253 df-neg 11254 df-nn 12020 df-2 12082 df-3 12083 df-4 12084 df-5 12085 df-6 12086 df-7 12087 df-8 12088 df-9 12089 df-n0 12280 df-z 12366 df-dec 12484 df-uz 12629 df-fz 13286 df-struct 16893 df-sets 16910 df-slot 16928 df-ndx 16940 df-base 16958 df-hom 17031 df-cco 17032 df-cat 17422 df-cid 17423 df-homf 17424 df-comf 17425 df-oppc 17466 df-func 17618 df-setc 17836 df-xpc 17934 df-curf 17977 df-hof 18013 df-yon 18014 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |