![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fuchom | Structured version Visualization version GIF version |
Description: The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) |
Ref | Expression |
---|---|
fucbas.q | ⊢ 𝑄 = (𝐶 FuncCat 𝐷) |
fuchom.n | ⊢ 𝑁 = (𝐶 Nat 𝐷) |
Ref | Expression |
---|---|
fuchom | ⊢ 𝑁 = (Hom ‘𝑄) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fucbas.q | . . . . 5 ⊢ 𝑄 = (𝐶 FuncCat 𝐷) | |
2 | eqid 2651 | . . . . 5 ⊢ (𝐶 Func 𝐷) = (𝐶 Func 𝐷) | |
3 | fuchom.n | . . . . 5 ⊢ 𝑁 = (𝐶 Nat 𝐷) | |
4 | eqid 2651 | . . . . 5 ⊢ (Base‘𝐶) = (Base‘𝐶) | |
5 | eqid 2651 | . . . . 5 ⊢ (comp‘𝐷) = (comp‘𝐷) | |
6 | simpl 472 | . . . . 5 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐶 ∈ Cat) | |
7 | simpr 476 | . . . . 5 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐷 ∈ Cat) | |
8 | eqid 2651 | . . . . . 6 ⊢ (comp‘𝑄) = (comp‘𝑄) | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | fuccofval 16666 | . . . . 5 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (comp‘𝑄) = (𝑣 ∈ ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)), ℎ ∈ (𝐶 Func 𝐷) ↦ ⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝐷)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))) |
10 | 1, 2, 3, 4, 5, 6, 7, 9 | fucval 16665 | . . . 4 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑄 = {〈(Base‘ndx), (𝐶 Func 𝐷)〉, 〈(Hom ‘ndx), 𝑁〉, 〈(comp‘ndx), (comp‘𝑄)〉}) |
11 | catstr 16664 | . . . 4 ⊢ {〈(Base‘ndx), (𝐶 Func 𝐷)〉, 〈(Hom ‘ndx), 𝑁〉, 〈(comp‘ndx), (comp‘𝑄)〉} Struct 〈1, ;15〉 | |
12 | homid 16122 | . . . 4 ⊢ Hom = Slot (Hom ‘ndx) | |
13 | snsstp2 4380 | . . . 4 ⊢ {〈(Hom ‘ndx), 𝑁〉} ⊆ {〈(Base‘ndx), (𝐶 Func 𝐷)〉, 〈(Hom ‘ndx), 𝑁〉, 〈(comp‘ndx), (comp‘𝑄)〉} | |
14 | ovex 6718 | . . . . . 6 ⊢ (𝐶 Nat 𝐷) ∈ V | |
15 | 3, 14 | eqeltri 2726 | . . . . 5 ⊢ 𝑁 ∈ V |
16 | 15 | a1i 11 | . . . 4 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 ∈ V) |
17 | eqid 2651 | . . . 4 ⊢ (Hom ‘𝑄) = (Hom ‘𝑄) | |
18 | 10, 11, 12, 13, 16, 17 | strfv3 15955 | . . 3 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (Hom ‘𝑄) = 𝑁) |
19 | 18 | eqcomd 2657 | . 2 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 = (Hom ‘𝑄)) |
20 | df-hom 16013 | . . . 4 ⊢ Hom = Slot ;14 | |
21 | 20 | str0 15958 | . . 3 ⊢ ∅ = (Hom ‘∅) |
22 | 3 | natffn 16656 | . . . . 5 ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) |
23 | funcrcl 16570 | . . . . . . . . . 10 ⊢ (𝑓 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) | |
24 | 23 | con3i 150 | . . . . . . . . 9 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ¬ 𝑓 ∈ (𝐶 Func 𝐷)) |
25 | 24 | eq0rdv 4012 | . . . . . . . 8 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Func 𝐷) = ∅) |
26 | 25 | xpeq2d 5173 | . . . . . . 7 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) = ((𝐶 Func 𝐷) × ∅)) |
27 | xp0 5587 | . . . . . . 7 ⊢ ((𝐶 Func 𝐷) × ∅) = ∅ | |
28 | 26, 27 | syl6eq 2701 | . . . . . 6 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) = ∅) |
29 | 28 | fneq2d 6020 | . . . . 5 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) ↔ 𝑁 Fn ∅)) |
30 | 22, 29 | mpbii 223 | . . . 4 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 Fn ∅) |
31 | fn0 6049 | . . . 4 ⊢ (𝑁 Fn ∅ ↔ 𝑁 = ∅) | |
32 | 30, 31 | sylib 208 | . . 3 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 = ∅) |
33 | fnfuc 16652 | . . . . . . 7 ⊢ FuncCat Fn (Cat × Cat) | |
34 | fndm 6028 | . . . . . . 7 ⊢ ( FuncCat Fn (Cat × Cat) → dom FuncCat = (Cat × Cat)) | |
35 | 33, 34 | ax-mp 5 | . . . . . 6 ⊢ dom FuncCat = (Cat × Cat) |
36 | 35 | ndmov 6860 | . . . . 5 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 FuncCat 𝐷) = ∅) |
37 | 1, 36 | syl5eq 2697 | . . . 4 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑄 = ∅) |
38 | 37 | fveq2d 6233 | . . 3 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (Hom ‘𝑄) = (Hom ‘∅)) |
39 | 21, 32, 38 | 3eqtr4a 2711 | . 2 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 = (Hom ‘𝑄)) |
40 | 19, 39 | pm2.61i 176 | 1 ⊢ 𝑁 = (Hom ‘𝑄) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 383 = wceq 1523 ∈ wcel 2030 Vcvv 3231 ∅c0 3948 {ctp 4214 〈cop 4216 × cxp 5141 dom cdm 5143 Fn wfn 5921 ‘cfv 5926 (class class class)co 6690 1c1 9975 4c4 11110 5c5 11111 ;cdc 11531 ndxcnx 15901 Basecbs 15904 Hom chom 15999 compcco 16000 Catccat 16372 Func cfunc 16561 Nat cnat 16648 FuncCat cfuc 16649 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-rep 4804 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-cnex 10030 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-mulcom 10038 ax-addass 10039 ax-mulass 10040 ax-distr 10041 ax-i2m1 10042 ax-1ne0 10043 ax-1rid 10044 ax-rnegex 10045 ax-rrecex 10046 ax-cnre 10047 ax-pre-lttri 10048 ax-pre-lttrn 10049 ax-pre-ltadd 10050 ax-pre-mulgt0 10051 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-fal 1529 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-nel 2927 df-ral 2946 df-rex 2947 df-reu 2948 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-pss 3623 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-tp 4215 df-op 4217 df-uni 4469 df-int 4508 df-iun 4554 df-br 4686 df-opab 4746 df-mpt 4763 df-tr 4786 df-id 5053 df-eprel 5058 df-po 5064 df-so 5065 df-fr 5102 df-we 5104 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-pred 5718 df-ord 5764 df-on 5765 df-lim 5766 df-suc 5767 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-riota 6651 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-om 7108 df-1st 7210 df-2nd 7211 df-wrecs 7452 df-recs 7513 df-rdg 7551 df-1o 7605 df-oadd 7609 df-er 7787 df-ixp 7951 df-en 7998 df-dom 7999 df-sdom 8000 df-fin 8001 df-pnf 10114 df-mnf 10115 df-xr 10116 df-ltxr 10117 df-le 10118 df-sub 10306 df-neg 10307 df-nn 11059 df-2 11117 df-3 11118 df-4 11119 df-5 11120 df-6 11121 df-7 11122 df-8 11123 df-9 11124 df-n0 11331 df-z 11416 df-dec 11532 df-uz 11726 df-fz 12365 df-struct 15906 df-ndx 15907 df-slot 15908 df-base 15910 df-hom 16013 df-cco 16014 df-func 16565 df-nat 16650 df-fuc 16651 |
This theorem is referenced by: fuccatid 16676 fucsect 16679 fuciso 16682 evlfcllem 16908 evlfcl 16909 curfcl 16919 uncf2 16924 curfuncf 16925 diag2cl 16933 curf2ndf 16934 yonedalem21 16960 yonedalem22 16965 yonedalem3b 16966 yonedalem3 16967 yonffthlem 16969 |
Copyright terms: Public domain | W3C validator |