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 16294

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 6527	. . . 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 16293	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) ↑_𝑚 (𝐻‘𝑧)))
7		funcf2.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
8		funcf2.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
9		opelxpi 5059	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
10	7, 8, 9	syl2anc 690	. . . . 5 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
11		fveq2 6085	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (1^st ‘𝑧) = (1^st ‘⟨𝑋, 𝑌⟩))
12	11	fveq2d 6089	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐹‘(1^st ‘𝑧)) = (𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)))
13		fveq2 6085	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (2^nd ‘𝑧) = (2^nd ‘⟨𝑋, 𝑌⟩))
14	13	fveq2d 6089	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐹‘(2^nd ‘𝑧)) = (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)))
15	12, 14	oveq12d 6542	. . . . . . 7 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → ((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) = ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))))
16		fveq2 6085	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐻‘𝑧) = (𝐻‘⟨𝑋, 𝑌⟩))
17		df-ov 6527	. . . . . . . 8 ⊢ (𝑋𝐻𝑌) = (𝐻‘⟨𝑋, 𝑌⟩)
18	16, 17	syl6eqr 2658	. . . . . . 7 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐻‘𝑧) = (𝑋𝐻𝑌))
19	15, 18	oveq12d 6542	. . . . . 6 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) ↑_𝑚 (𝐻‘𝑧)) = (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_𝑚 (𝑋𝐻𝑌)))
20	19	fvixp 7773	. . . . 5 ⊢ ((𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑧))𝐽(𝐹‘(2^nd ‘𝑧))) ↑_𝑚 (𝐻‘𝑧)) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵)) → (𝐺‘⟨𝑋, 𝑌⟩) ∈ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_𝑚 (𝑋𝐻𝑌)))
21	6, 10, 20	syl2anc 690	. . . 4 ⊢ (𝜑 → (𝐺‘⟨𝑋, 𝑌⟩) ∈ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_𝑚 (𝑋𝐻𝑌)))
22	1, 21	syl5eqel 2688	. . 3 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_𝑚 (𝑋𝐻𝑌)))
23		op1stg 7045	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (1^st ‘⟨𝑋, 𝑌⟩) = 𝑋)
24	23	fveq2d 6089	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(1^st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋))
25		op2ndg 7046	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (2^nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
26	25	fveq2d 6089	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))
27	24, 26	oveq12d 6542	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) = ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
28	7, 8, 27	syl2anc 690	. . . 4 ⊢ (𝜑 → ((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) = ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
29	28	oveq1d 6539	. . 3 ⊢ (𝜑 → (((𝐹‘(1^st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2^nd ‘⟨𝑋, 𝑌⟩))) ↑_𝑚 (𝑋𝐻𝑌)) = (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑_𝑚 (𝑋𝐻𝑌)))
30	22, 29	eleqtrd 2686	. 2 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑_𝑚 (𝑋𝐻𝑌)))
31		elmapi 7739	. 2 ⊢ ((𝑋𝐺𝑌) ∈ (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑_𝑚 (𝑋𝐻𝑌)) → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
32	30, 31	syl 17	1 ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 382 = wceq 1474 ∈ wcel 1976 ⟨cop 4127 class class class wbr 4574 × cxp 5023 ⟶wf 5783 ‘cfv 5787 (class class class)co 6524 1^st c1st 7031 2^nd c2nd 7032 ↑_𝑚 cmap 7718 Xcixp 7768 Basecbs 15638 Hom chom 15722 Func cfunc 16280

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 2032 ax-13 2229 ax-ext 2586 ax-rep 4690 ax-sep 4700 ax-nul 4709 ax-pow 4761 ax-pr 4825 ax-un 6821

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 2458 df-mo 2459 df-clab 2593 df-cleq 2599 df-clel 2602 df-nfc 2736 df-ne 2778 df-ral 2897 df-rex 2898 df-reu 2899 df-rab 2901 df-v 3171 df-sbc 3399 df-csb 3496 df-dif 3539 df-un 3541 df-in 3543 df-ss 3550 df-nul 3871 df-if 4033 df-pw 4106 df-sn 4122 df-pr 4124 df-op 4128 df-uni 4364 df-iun 4448 df-br 4575 df-opab 4635 df-mpt 4636 df-id 4940 df-xp 5031 df-rel 5032 df-cnv 5033 df-co 5034 df-dm 5035 df-rn 5036 df-res 5037 df-ima 5038 df-iota 5751 df-fun 5789 df-fn 5790 df-f 5791 df-f1 5792 df-fo 5793 df-f1o 5794 df-fv 5795 df-ov 6527 df-oprab 6528 df-mpt2 6529 df-1st 7033 df-2nd 7034 df-map 7720 df-ixp 7769 df-func 16284

This theorem is referenced by: funcsect 16298 funcoppc 16301 cofu2 16312 cofucl 16314 cofulid 16316 cofurid 16317 funcres 16322 funcres2 16324 funcres2c 16327 isfull2 16337 isfth2 16341 fthsect 16351 fthmon 16353 fuccocl 16390 fucidcl 16391 invfuc 16400 natpropd 16402 catciso 16523 prfval 16605 prfcl 16609 prf1st 16610 prf2nd 16611 1st2ndprf 16612 evlfcllem 16627 evlfcl 16628 curf1cl 16634 curf2cl 16637 uncf2 16643 curfuncf 16644 uncfcurf 16645 diag2cl 16652 curf2ndf 16653 yonedalem4c 16683 yonedalem3b 16685 yonedainv 16687 yonffthlem 16688

W3C validator