| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > funcrcl | Structured version Visualization version GIF version | ||
| Description: Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| Ref | Expression |
|---|---|
| funcrcl | ⊢ (𝐹 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-func 17919 | . 2 ⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) | |
| 2 | 1 | elmpocl 7651 | 1 ⊢ (𝐹 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ∀wral 3079 [wsbc 3744 〈cop 4595 {copab 5173 × cxp 5659 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 1st c1st 7980 2nd c2nd 7981 ↑m cmap 8820 Xcixp 8891 Basecbs 17273 Hom chom 17325 compcco 17326 Catccat 17724 Idccid 17725 Func cfunc 17915 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pr 5404 |
| This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-br 5110 df-opab 5174 df-xp 5667 df-dm 5671 df-iota 6492 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-func 17919 |
| This theorem is used by: funcf1 17927 funcixp 17928 funcid 17931 funcco 17932 funcsect 17933 funcinv 17934 funciso 17935 funcoppc 17936 cofucl 17949 cofulid 17951 cofurid 17952 funcres 17957 funcres2b 17958 funcpropd 17963 funcres2c 17964 isfull 17973 isfth 17977 fthsect 17988 fthinv 17989 fthmon 17990 fthepi 17991 ffthiso 17992 natfval 18010 fucbas 18024 fuchom 18025 fucco 18026 fuccocl 18028 fucidcl 18029 fuclid 18030 fucrid 18031 fucass 18032 fucid 18035 fucsect 18036 fucinv 18037 invfuc 18038 fuciso 18039 funcsetcres2 18154 prfcl 18263 prf1st 18264 prf2nd 18265 curf1cl 18288 curfcl 18292 uncfval 18294 uncfcl 18295 uncf1 18296 uncf2 18297 curfuncf 18298 uncfcurf 18299 yonffthlem 18342 yoneda 18343 funcrcl2 49885 funcrcl3 49886 initc 49897 prcofpropd 50185 termc2 50324 euendfunc 50332 lanpropd 50421 ranpropd 50422 ranval3 50437 lmddu 50473 cmddu 50474 |
| Copyright terms: Public domain | W3C validator |