![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relfunc | Structured version Visualization version GIF version |
Description: The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
Ref | Expression |
---|---|
relfunc | ⊢ Rel (𝐷 Func 𝐸) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-func 16989 | . 2 ⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) | |
2 | 1 | relmpoopab 7599 | 1 ⊢ Rel (𝐷 Func 𝐸) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ∀wral 3088 [wsbc 3683 〈cop 4448 × cxp 5406 Rel wrel 5413 ⟶wf 6186 ‘cfv 6190 (class class class)co 6978 1st c1st 7501 2nd c2nd 7502 ↑𝑚 cmap 8208 Xcixp 8261 Basecbs 16342 Hom chom 16435 compcco 16436 Catccat 16796 Idccid 16797 Func cfunc 16985 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-iun 4795 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-iota 6154 df-fun 6192 df-fv 6198 df-ov 6981 df-oprab 6982 df-mpo 6983 df-1st 7503 df-2nd 7504 df-func 16989 |
This theorem is referenced by: cofuval 17013 cofu1 17015 cofu2 17017 cofuval2 17018 cofucl 17019 cofuass 17020 cofulid 17021 cofurid 17022 funcres 17027 funcres2 17029 wunfunc 17030 funcpropd 17031 relfull 17039 relfth 17040 isfull 17041 isfth 17045 idffth 17064 cofull 17065 cofth 17066 ressffth 17069 isnat 17078 isnat2 17079 nat1st2nd 17082 fuccocl 17095 fucidcl 17096 fuclid 17097 fucrid 17098 fucass 17099 fucsect 17103 fucinv 17104 invfuc 17105 fuciso 17106 natpropd 17107 fucpropd 17108 catciso 17228 prfval 17310 prfcl 17314 prf1st 17315 prf2nd 17316 1st2ndprf 17317 evlfcllem 17332 evlfcl 17333 curf1cl 17339 curf2cl 17342 curfcl 17343 uncf1 17347 uncf2 17348 curfuncf 17349 uncfcurf 17350 diag1cl 17353 diag2cl 17357 curf2ndf 17358 yon1cl 17374 oyon1cl 17382 yonedalem1 17383 yonedalem21 17384 yonedalem3a 17385 yonedalem4c 17388 yonedalem22 17389 yonedalem3b 17390 yonedalem3 17391 yonedainv 17392 yonffthlem 17393 yoniso 17396 |
Copyright terms: Public domain | W3C validator |