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 17120 | . 2 ⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) | |
2 | 1 | relmpoopab 7781 | 1 ⊢ Rel (𝐷 Func 𝐸) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 398 ∧ w3a 1082 = wceq 1531 ∈ wcel 2108 ∀wral 3136 [wsbc 3770 〈cop 4565 × cxp 5546 Rel wrel 5553 ⟶wf 6344 ‘cfv 6348 (class class class)co 7148 1st c1st 7679 2nd c2nd 7680 ↑m cmap 8398 Xcixp 8453 Basecbs 16475 Hom chom 16568 compcco 16569 Catccat 16927 Idccid 16928 Func cfunc 17116 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7453 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-sbc 3771 df-csb 3882 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4831 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6307 df-fun 6350 df-fv 6356 df-ov 7151 df-oprab 7152 df-mpo 7153 df-1st 7681 df-2nd 7682 df-func 17120 |
This theorem is referenced by: cofuval 17144 cofu1 17146 cofu2 17148 cofuval2 17149 cofucl 17150 cofuass 17151 cofulid 17152 cofurid 17153 funcres 17158 funcres2 17160 wunfunc 17161 funcpropd 17162 relfull 17170 relfth 17171 isfull 17172 isfth 17176 idffth 17195 cofull 17196 cofth 17197 ressffth 17200 isnat 17209 isnat2 17210 nat1st2nd 17213 fuccocl 17226 fucidcl 17227 fuclid 17228 fucrid 17229 fucass 17230 fucsect 17234 fucinv 17235 invfuc 17236 fuciso 17237 natpropd 17238 fucpropd 17239 catciso 17359 prfval 17441 prfcl 17445 prf1st 17446 prf2nd 17447 1st2ndprf 17448 evlfcllem 17463 evlfcl 17464 curf1cl 17470 curf2cl 17473 curfcl 17474 uncf1 17478 uncf2 17479 curfuncf 17480 uncfcurf 17481 diag1cl 17484 diag2cl 17488 curf2ndf 17489 yon1cl 17505 oyon1cl 17513 yonedalem1 17514 yonedalem21 17515 yonedalem3a 17516 yonedalem4c 17519 yonedalem22 17520 yonedalem3b 17521 yonedalem3 17522 yonedainv 17523 yonffthlem 17524 yoniso 17527 |
Copyright terms: Public domain | W3C validator |