Theorem funcf2 16728

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 6873	. . . 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 16727	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚 (𝐻‘𝑧)))
7		funcf2.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
8		funcf2.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
9		opelxpi 5348	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
10	7, 8, 9	syl2anc 575	. . . . 5 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
11		2fveq3 6409	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐹‘(1st ‘𝑧)) = (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)))
12		2fveq3 6409	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐹‘(2nd ‘𝑧)) = (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)))
13	11, 12	oveq12d 6888	. . . . . . 7 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → ((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) = ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2nd ‘⟨𝑋, 𝑌⟩))))
14		fveq2 6404	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐻‘𝑧) = (𝐻‘⟨𝑋, 𝑌⟩))
15		df-ov 6873	. . . . . . . 8 ⊢ (𝑋𝐻𝑌) = (𝐻‘⟨𝑋, 𝑌⟩)
16	14, 15	syl6eqr 2858	. . . . . . 7 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (𝐻‘𝑧) = (𝑋𝐻𝑌))
17	13, 16	oveq12d 6888	. . . . . 6 ⊢ (𝑧 = ⟨𝑋, 𝑌⟩ → (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚 (𝐻‘𝑧)) = (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2nd ‘⟨𝑋, 𝑌⟩))) ↑𝑚 (𝑋𝐻𝑌)))
18	17	fvixp 8146	. . . . 5 ⊢ ((𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚 (𝐻‘𝑧)) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵)) → (𝐺‘⟨𝑋, 𝑌⟩) ∈ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2nd ‘⟨𝑋, 𝑌⟩))) ↑𝑚 (𝑋𝐻𝑌)))
19	6, 10, 18	syl2anc 575	. . . 4 ⊢ (𝜑 → (𝐺‘⟨𝑋, 𝑌⟩) ∈ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2nd ‘⟨𝑋, 𝑌⟩))) ↑𝑚 (𝑋𝐻𝑌)))
20	1, 19	syl5eqel 2889	. . 3 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2nd ‘⟨𝑋, 𝑌⟩))) ↑𝑚 (𝑋𝐻𝑌)))
21		op1stg 7406	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
22	21	fveq2d 6408	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑋))
23		op2ndg 7407	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
24	23	fveq2d 6408	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹‘𝑌))
25	22, 24	oveq12d 6888	. . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2nd ‘⟨𝑋, 𝑌⟩))) = ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
26	7, 8, 25	syl2anc 575	. . . 4 ⊢ (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2nd ‘⟨𝑋, 𝑌⟩))) = ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
27	26	oveq1d 6885	. . 3 ⊢ (𝜑 → (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩))𝐽(𝐹‘(2nd ‘⟨𝑋, 𝑌⟩))) ↑𝑚 (𝑋𝐻𝑌)) = (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑𝑚 (𝑋𝐻𝑌)))
28	20, 27	eleqtrd 2887	. 2 ⊢ (𝜑 → (𝑋𝐺𝑌) ∈ (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑𝑚 (𝑋𝐻𝑌)))
29		elmapi 8110	. 2 ⊢ ((𝑋𝐺𝑌) ∈ (((𝐹‘𝑋)𝐽(𝐹‘𝑌)) ↑𝑚 (𝑋𝐻𝑌)) → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
30	28, 29	syl 17	1 ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637   ∈ wcel 2156  ⟨cop 4376   class class class wbr 4844   × cxp 5309  ⟶wf 6093  ‘cfv 6097  (class class class)co 6870  1^st c1st 7392  2^nd c2nd 7393   ↑_𝑚 cmap 8088  Xcixp 8141  Basecbs 16064  Hom chom 16160   Func cfunc 16714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-1st 7394  df-2nd 7395  df-map 8090  df-ixp 8142  df-func 16718

This theorem is referenced by:  funcsect  16732  funcoppc  16735  cofu2  16746  cofucl  16748  cofulid  16750  cofurid  16751  funcres  16756  funcres2  16758  funcres2c  16761  isfull2  16771  isfth2  16775  fthsect  16785  fthmon  16787  fuccocl  16824  fucidcl  16825  invfuc  16834  natpropd  16836  catciso  16957  prfval  17040  prfcl  17044  prf1st  17045  prf2nd  17046  1st2ndprf  17047  evlfcllem  17062  evlfcl  17063  curf1cl  17069  curf2cl  17072  uncf2  17078  curfuncf  17079  uncfcurf  17080  diag2cl  17087  curf2ndf  17088  yonedalem4c  17118  yonedalem3b  17120  yonedainv  17122  yonffthlem  17123