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 16295

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 2609	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
5		eqid 2609	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
6		eqid 2609	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
7		eqid 2609	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
8		eqid 2609	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
9		eqid 2609	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
10		df-br 4578	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 206	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 16292	. . . . . 6 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
14	13	simpld 473	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
15	13	simprd 477	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
16	2, 3, 4, 5, 6, 7, 8, 9, 14, 15	isfunc 16293	. . 3 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2^nd ‘𝑧))) ↑_𝑚 ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
17	1, 16	mpbid 220	. 2 ⊢ (𝜑 → (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2^nd ‘𝑧))) ↑_𝑚 ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
18	17	simp1d 1065	1 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1030 = wceq 1474 ∈ wcel 1976 ∀wral 2895 ⟨cop 4130 class class class wbr 4577 × cxp 5026 ⟶wf 5786 ‘cfv 5790 (class class class)co 6527 1^st c1st 7034 2^nd c2nd 7035 ↑_𝑚 cmap 7721 Xcixp 7771 Basecbs 15641 Hom chom 15725 compcco 15726 Catccat 16094 Idccid 16095 Func cfunc 16283

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1712 ax-4 1727 ax-5 1826 ax-6 1874 ax-7 1921 ax-8 1978 ax-9 1985 ax-10 2005 ax-11 2020 ax-12 2033 ax-13 2233 ax-ext 2589 ax-rep 4693 ax-sep 4703 ax-nul 4712 ax-pow 4764 ax-pr 4828 ax-un 6824

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3an 1032 df-tru 1477 df-ex 1695 df-nf 1700 df-sb 1867 df-eu 2461 df-mo 2462 df-clab 2596 df-cleq 2602 df-clel 2605 df-nfc 2739 df-ne 2781 df-ral 2900 df-rex 2901 df-reu 2902 df-rab 2904 df-v 3174 df-sbc 3402 df-csb 3499 df-dif 3542 df-un 3544 df-in 3546 df-ss 3553 df-nul 3874 df-if 4036 df-pw 4109 df-sn 4125 df-pr 4127 df-op 4131 df-uni 4367 df-iun 4451 df-br 4578 df-opab 4638 df-mpt 4639 df-id 4943 df-xp 5034 df-rel 5035 df-cnv 5036 df-co 5037 df-dm 5038 df-rn 5039 df-res 5040 df-ima 5041 df-iota 5754 df-fun 5792 df-fn 5793 df-f 5794 df-f1 5795 df-fo 5796 df-f1o 5797 df-fv 5798 df-ov 6530 df-oprab 6531 df-mpt2 6532 df-map 7723 df-ixp 7772 df-func 16287

This theorem is referenced by: funcsect 16301 funcinv 16302 funciso 16303 funcoppc 16304 cofu1 16313 cofucl 16317 cofuass 16318 cofulid 16319 cofurid 16320 funcres 16325 funcres2 16327 wunfunc 16328 funcres2c 16330 fullpropd 16349 fthsect 16354 fthinv 16355 fthmon 16356 ffthiso 16358 cofull 16363 cofth 16364 fuccocl 16393 fucidcl 16394 fuclid 16395 fucrid 16396 fucass 16397 fucsect 16401 fucinv 16402 invfuc 16403 fuciso 16404 natpropd 16405 fucpropd 16406 catciso 16526 prfval 16608 prfcl 16612 prf1st 16613 prf2nd 16614 1st2ndprf 16615 evlfcllem 16630 evlfcl 16631 curf1cl 16637 curfcl 16641 uncf1 16645 uncf2 16646 curfuncf 16647 uncfcurf 16648 diag1cl 16651 curf2ndf 16656 yon1cl 16672 oyon1cl 16680 yonedalem3a 16683 yonedalem4c 16686 yonedalem3b 16688 yonedalem3 16689 yonedainv 16690 yonffthlem 16691 yoniso 16694

W3C validator