funcf2 - Metamath Proof Explorer

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

Theorem funcf2 17887

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

**Hypotheses**
Ref	Expression
funcixp.b	⊢ 𝐵 = (Base‘𝐷)
funcixp.h	⊢ 𝐻 = (Hom ‘𝐷)
funcixp.j	⊢ 𝐽 = (Hom ‘𝐸)
funcixp.f	⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
funcf2.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
funcf2.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)

**Assertion**
Ref	Expression
funcf2	⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))

Proof of Theorem funcf2 Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ov 7427	. . . 4 ⊢ (𝑋𝐺𝑌) = (𝐺‘⟨𝑋, 𝑌⟩)
2		funcixp.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐷)
3		funcixp.h	. . . . . 6 ⊢ 𝐻 = (Hom ‘𝐷)
4		funcixp.j	. . . . . 6 ⊢ 𝐽 = (Hom ‘𝐸)
5		funcixp.f	. . . . . 6 ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
6	2, 3, 4, 5	funcixp 17886	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) ↑_m (𝐻‘𝑧)))
7		funcf2.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
8		funcf2.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
9	7, 8	opelxpd 5721	. . . . 5 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
10		2fveq3 6906	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐹‘(1^st ‘𝑧)) = (𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)))
11		2fveq3 6906	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐹‘(2^nd ‘𝑧)) = (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)))
12	10, 11	oveq12d 7442	. . . . . . 7 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → ((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) = ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))))
13		fveq2 6901	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐻‘𝑧) = (𝐻‘⟨𝑋, 𝑌⟩))
14		df-ov 7427	. . . . . . . 8 ⊢ (𝑋𝐻𝑌) = (𝐻‘⟨𝑋, 𝑌⟩)
15	13, 14	eqtr4di 2784	. . . . . . 7 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐻‘𝑧) = (𝑋𝐻𝑌))
16	12, 15	oveq12d 7442	. . . . . 6 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) ↑_m (𝐻‘𝑧)) = (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)))
17	16	fvixp 8931	. . . . 5 ⊢ ((𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) ↑_m (𝐻‘𝑧)) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵)) → (𝐺‘⟨𝑋, 𝑌⟩) ∈ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)))
18	6, 9, 17	syl2anc 582	. . . 4 ⊢ (𝜑 → (𝐺‘⟨𝑋, 𝑌⟩) ∈ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)))
19	1, 18	eqeltrid 2830	. . 3 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)))
20		op1stg 8015	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (1^st ‘⟨𝑋, 𝑌⟩) = 𝑋)
21	20	fveq2d 6905	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋))
22		op2ndg 8016	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (2^nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
23	22	fveq2d 6905	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))
24	21, 23	oveq12d 7442	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) = ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
25	7, 8, 24	syl2anc 582	. . . 4 ⊢ (𝜑 → ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) = ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
26	25	oveq1d 7439	. . 3 ⊢ (𝜑 → (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)) = (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑_m (𝑋𝐻𝑌)))
27	19, 26	eleqtrd 2828	. 2 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑_m (𝑋𝐻𝑌)))
28		elmapi 8878	. 2 ⊢ ((𝑋𝐺𝑌) ∈ (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑_m (𝑋𝐻𝑌)) → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
29	27, 28	syl 17	1 ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ⟨cop 4639 class class class wbr 5153 × cxp 5680 ⟶wf 6550 ‘cfv 6554 (class class class)co 7424 1^st c1st 8001 2^nd c2nd 8002 ↑_m cmap 8855 Xcixp 8926 Basecbs 17213 Hom chom 17277 Func cfunc 17873

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-fv 6562 df-ov 7427 df-oprab 7428 df-mpo 7429 df-1st 8003 df-2nd 8004 df-map 8857 df-ixp 8927 df-func 17877

This theorem is referenced by: funcsect 17891 funcoppc 17894 cofu2 17905 cofucl 17907 cofulid 17909 cofurid 17910 funcres 17915 funcres2 17917 funcres2c 17923 isfull2 17933 isfth2 17937 fthsect 17947 fthmon 17949 fuccocl 17989 fucidcl 17990 invfuc 17999 natpropd 18001 catciso 18133 prfval 18223 prfcl 18227 prf1st 18228 prf2nd 18229 1st2ndprf 18230 evlfcllem 18246 evlfcl 18247 curf1cl 18253 curf2cl 18256 uncf2 18262 curfuncf 18263 uncfcurf 18264 diag2cl 18271 curf2ndf 18272 yonedalem4c 18302 yonedalem3b 18304 yonedainv 18306 yonffthlem 18307 fullthinc 48367 fullthinc2 48368 thincfth 48369 thincciso 48370

W3C validator