funcf1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > funcf1		Structured version Visualization version GIF version

Theorem funcf1 16573

Description: The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017.)

**Hypotheses**
Ref	Expression
funcf1.b	⊢ 𝐵 = (Base‘𝐷)
funcf1.c	⊢ 𝐶 = (Base‘𝐸)
funcf1.f	⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)

**Assertion**
Ref	Expression
funcf1	⊢ (𝜑 → 𝐹:𝐵⟶𝐶)

Proof of Theorem funcf1 Dummy variables 𝑚 𝑛 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funcf1.f	. . 3 ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
2		funcf1.b	. . . 4 ⊢ 𝐵 = (Base‘𝐷)
3		funcf1.c	. . . 4 ⊢ 𝐶 = (Base‘𝐸)
4		eqid 2651	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
5		eqid 2651	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
6		eqid 2651	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
7		eqid 2651	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
8		eqid 2651	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
9		eqid 2651	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
10		df-br 4686	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 208	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 16570	. . . . . 6 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
14	13	simpld 474	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
15	13	simprd 478	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
16	2, 3, 4, 5, 6, 7, 8, 9, 14, 15	isfunc 16571	. . 3 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2^nd ‘𝑧))) ↑_𝑚 ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
17	1, 16	mpbid 222	. 2 ⊢ (𝜑 → (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2^nd ‘𝑧))) ↑_𝑚 ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
18	17	simp1d 1093	1 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 = wceq 1523 ∈ wcel 2030 ∀wral 2941 ⟨cop 4216 class class class wbr 4685 × cxp 5141 ⟶wf 5922 ‘cfv 5926 (class class class)co 6690 1^st c1st 7208 2^nd c2nd 7209 ↑_𝑚 cmap 7899 Xcixp 7950 Basecbs 15904 Hom chom 15999 compcco 16000 Catccat 16372 Idccid 16373 Func cfunc 16561

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

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 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-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-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-iun 4554 df-br 4686 df-opab 4746 df-mpt 4763 df-id 5053 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-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-map 7901 df-ixp 7951 df-func 16565

This theorem is referenced by: funcsect 16579 funcinv 16580 funciso 16581 funcoppc 16582 cofu1 16591 cofucl 16595 cofuass 16596 cofulid 16597 cofurid 16598 funcres 16603 funcres2 16605 wunfunc 16606 funcres2c 16608 fullpropd 16627 fthsect 16632 fthinv 16633 fthmon 16634 ffthiso 16636 cofull 16641 cofth 16642 fuccocl 16671 fucidcl 16672 fuclid 16673 fucrid 16674 fucass 16675 fucsect 16679 fucinv 16680 invfuc 16681 fuciso 16682 natpropd 16683 fucpropd 16684 catciso 16804 prfval 16886 prfcl 16890 prf1st 16891 prf2nd 16892 1st2ndprf 16893 evlfcllem 16908 evlfcl 16909 curf1cl 16915 curfcl 16919 uncf1 16923 uncf2 16924 curfuncf 16925 uncfcurf 16926 diag1cl 16929 curf2ndf 16934 yon1cl 16950 oyon1cl 16958 yonedalem3a 16961 yonedalem4c 16964 yonedalem3b 16966 yonedalem3 16967 yonedainv 16968 yonffthlem 16969 yoniso 16972

W3C validator