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 17855

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 2725	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
5		eqid 2725	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
6		eqid 2725	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
7		eqid 2725	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
8		eqid 2725	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
9		eqid 2725	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
10		df-br 5150	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 217	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 17852	. . . . . 6 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
14	13	simpld 493	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
15	13	simprd 494	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
16	2, 3, 4, 5, 6, 7, 8, 9, 14, 15	isfunc 17853	. . 3 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
17	1, 16	mpbid 231	. 2 ⊢ (𝜑 → (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
18	17	simp1d 1139	1 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∀wral 3050 ⟨cop 4636 class class class wbr 5149 × cxp 5676 ⟶wf 6545 ‘cfv 6549 (class class class)co 7419 1^st c1st 7992 2^nd c2nd 7993 ↑_m cmap 8845 Xcixp 8916 Basecbs 17183 Hom chom 17247 compcco 17248 Catccat 17647 Idccid 17648 Func cfunc 17843

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-iun 4999 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-fv 6557 df-ov 7422 df-oprab 7423 df-mpo 7424 df-map 8847 df-ixp 8917 df-func 17847

This theorem is referenced by: funcsect 17861 funcinv 17862 funciso 17863 funcoppc 17864 cofu1 17873 cofucl 17877 cofuass 17878 cofulid 17879 cofurid 17880 funcres 17885 funcres2 17887 wunfunc 17890 wunfuncOLD 17891 funcres2c 17893 fullpropd 17912 fthsect 17917 fthinv 17918 fthmon 17919 ffthiso 17921 cofull 17926 cofth 17927 fuccocl 17959 fucidcl 17960 fuclid 17961 fucrid 17962 fucass 17963 fucsect 17967 fucinv 17968 invfuc 17969 fuciso 17970 natpropd 17971 fucpropd 17972 catciso 18103 prfval 18193 prfcl 18197 prf1st 18198 prf2nd 18199 1st2ndprf 18200 evlfcllem 18216 evlfcl 18217 curf1cl 18223 curfcl 18227 uncf1 18231 uncf2 18232 curfuncf 18233 uncfcurf 18234 diag1cl 18237 curf2ndf 18242 yon1cl 18258 oyon1cl 18266 yonedalem3a 18269 yonedalem4c 18272 yonedalem3b 18274 yonedalem3 18275 yonedainv 18276 yonffthlem 18277 yoniso 18280 fullthinc 48238

W3C validator