hof2fval

Description: The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W ), yields a function (a morphism of SetCat ) mapping h : X --> Y to g o. h o. f : Z --> W . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	⊢ 𝑀 = ( Hom_F ‘ 𝐶 )
	hofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	hof1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	hof1.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	hof1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	hof1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	hof2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	hof2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
	hof2.o	⊢ · = ( comp ‘ 𝐶 )
Assertion	hof2fval	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( 𝑓 ∈ ( 𝑍 𝐻 𝑋 ) , 𝑔 ∈ ( 𝑌 𝐻 𝑊 ) ↦ ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hofval.m	⊢ 𝑀 = ( Hom_F ‘ 𝐶 )
2		hofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		hof1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		hof1.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
5		hof1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		hof1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		hof2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		hof2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
9		hof2.o	⊢ · = ( comp ‘ 𝐶 )
10	1 2 3 4 9	hofval	⊢ ( 𝜑 → 𝑀 = ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )
11		fvex	⊢ ( Hom_f ‘ 𝐶 ) ∈ V
12	3	fvexi	⊢ 𝐵 ∈ V
13	12 12	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
14	13 13	mpoex	⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ∈ V
15	11 14	op2ndd	⊢ ( 𝑀 = ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ → ( 2^nd ‘ 𝑀 ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) )
16	10 15	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝑀 ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) )
17		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 1^st ‘ 𝑦 ) = ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) )
19		op1stg	⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑍 )
20	7 8 19	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑍 )
21	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑍 )
22	18 21	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 1^st ‘ 𝑦 ) = 𝑍 )
23		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ )
24	23	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
25		op1stg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
26	5 6 25	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
27	26	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
28	24 27	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 1^st ‘ 𝑥 ) = 𝑋 )
29	22 28	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) = ( 𝑍 𝐻 𝑋 ) )
30	23	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
31		op2ndg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
32	5 6 31	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
33	32	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
34	30 33	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 2^nd ‘ 𝑥 ) = 𝑌 )
35	17	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 2^nd ‘ 𝑦 ) = ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) )
36		op2ndg	⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑊 )
37	7 8 36	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑊 )
38	37	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑊 )
39	35 38	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 2^nd ‘ 𝑦 ) = 𝑊 )
40	34 39	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) = ( 𝑌 𝐻 𝑊 ) )
41	23	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
42		df-ov	⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
43	41 42	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 𝐻 ‘ 𝑥 ) = ( 𝑋 𝐻 𝑌 ) )
44	22 28	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ = ⟨ 𝑍 , 𝑋 ⟩ )
45	44 39	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) = ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) )
46	23 39	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) )
47	46	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) = ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) )
48		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → 𝑓 = 𝑓 )
49	45 47 48	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) = ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) )
50	43 49	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) ) )
51	29 40 50	mpoeq123dv	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = ⟨ 𝑍 , 𝑊 ⟩ ) ) → ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) = ( 𝑓 ∈ ( 𝑍 𝐻 𝑋 ) , 𝑔 ∈ ( 𝑌 𝐻 𝑊 ) ↦ ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) ) ) )
52	5 6	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
53	7 8	opelxpd	⊢ ( 𝜑 → ⟨ 𝑍 , 𝑊 ⟩ ∈ ( 𝐵 × 𝐵 ) )
54		ovex	⊢ ( 𝑍 𝐻 𝑋 ) ∈ V
55		ovex	⊢ ( 𝑌 𝐻 𝑊 ) ∈ V
56	54 55	mpoex	⊢ ( 𝑓 ∈ ( 𝑍 𝐻 𝑋 ) , 𝑔 ∈ ( 𝑌 𝐻 𝑊 ) ↦ ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) ) ) ∈ V
57	56	a1i	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑍 𝐻 𝑋 ) , 𝑔 ∈ ( 𝑌 𝐻 𝑊 ) ↦ ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) ) ) ∈ V )
58	16 51 52 53 57	ovmpod	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( 𝑓 ∈ ( 𝑍 𝐻 𝑋 ) , 𝑔 ∈ ( 𝑌 𝐻 𝑊 ) ↦ ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝑓 ) ) ) )

Metamath Proof Explorer

Theorem hof2fval

Proof