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 17690

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 7353	. . . 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 17689	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) ↑_m (𝐻‘𝑧)))
7		funcf2.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
8		funcf2.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
9	7, 8	opelxpd 5669	. . . . 5 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
10		2fveq3 6843	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐹‘(1^st ‘𝑧)) = (𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)))
11		2fveq3 6843	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐹‘(2^nd ‘𝑧)) = (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)))
12	10, 11	oveq12d 7368	. . . . . . 7 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → ((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) = ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))))
13		fveq2 6838	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐻‘𝑧) = (𝐻‘⟨𝑋, 𝑌⟩))
14		df-ov 7353	. . . . . . . 8 ⊢ (𝑋𝐻𝑌) = (𝐻‘⟨𝑋, 𝑌⟩)
15	13, 14	eqtr4di 2796	. . . . . . 7 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐻‘𝑧) = (𝑋𝐻𝑌))
16	12, 15	oveq12d 7368	. . . . . 6 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) ↑_m (𝐻‘𝑧)) = (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)))
17	16	fvixp 8774	. . . . 5 ⊢ ((𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) ↑_m (𝐻‘𝑧)) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵)) → (𝐺‘⟨𝑋, 𝑌⟩) ∈ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)))
18	6, 9, 17	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝐺‘⟨𝑋, 𝑌⟩) ∈ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)))
19	1, 18	eqeltrid 2843	. . 3 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)))
20		op1stg 7924	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (1^st ‘⟨𝑋, 𝑌⟩) = 𝑋)
21	20	fveq2d 6842	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋))
22		op2ndg 7925	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (2^nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
23	22	fveq2d 6842	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))
24	21, 23	oveq12d 7368	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) = ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
25	7, 8, 24	syl2anc 585	. . . 4 ⊢ (𝜑 → ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) = ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
26	25	oveq1d 7365	. . 3 ⊢ (𝜑 → (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_m (𝑋𝐻𝑌)) = (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑_m (𝑋𝐻𝑌)))
27	19, 26	eleqtrd 2841	. 2 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑_m (𝑋𝐻𝑌)))
28		elmapi 8721	. 2 ⊢ ((𝑋𝐺𝑌) ∈ (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑_m (𝑋𝐻𝑌)) → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
29	27, 28	syl 17	1 ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ⟨cop 4591 class class class wbr 5104 × cxp 5629 ⟶wf 6488 ‘cfv 6492 (class class class)co 7350 1^st c1st 7910 2^nd c2nd 7911 ↑_m cmap 8699 Xcixp 8769 Basecbs 17019 Hom chom 17080 Func cfunc 17676

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-rep 5241 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7663

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6444 df-fun 6494 df-fn 6495 df-f 6496 df-fv 6500 df-ov 7353 df-oprab 7354 df-mpo 7355 df-1st 7912 df-2nd 7913 df-map 8701 df-ixp 8770 df-func 17680

This theorem is referenced by: funcsect 17694 funcoppc 17697 cofu2 17708 cofucl 17710 cofulid 17712 cofurid 17713 funcres 17718 funcres2 17720 funcres2c 17724 isfull2 17734 isfth2 17738 fthsect 17748 fthmon 17750 fuccocl 17789 fucidcl 17790 invfuc 17799 natpropd 17801 catciso 17933 prfval 18023 prfcl 18027 prf1st 18028 prf2nd 18029 1st2ndprf 18030 evlfcllem 18046 evlfcl 18047 curf1cl 18053 curf2cl 18056 uncf2 18062 curfuncf 18063 uncfcurf 18064 diag2cl 18071 curf2ndf 18072 yonedalem4c 18102 yonedalem3b 18104 yonedainv 18106 yonffthlem 18107 fullthinc 46857 fullthinc2 46858 thincfth 46859 thincciso 46860

W3C validator