hofval

Description: Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from ( oppCatC ) X. C to SetCat , whose object part is the hom-function Hom , and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	⊢ 𝑀 = ( Hom_F ‘ 𝐶 )
	hofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	hofval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	hofval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	hofval.o	⊢ · = ( comp ‘ 𝐶 )
Assertion	hofval	⊢ ( 𝜑 → 𝑀 = ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		hofval.m	⊢ 𝑀 = ( Hom_F ‘ 𝐶 )
2		hofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		hofval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		hofval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
5		hofval.o	⊢ · = ( comp ‘ 𝐶 )
6		df-hof	⊢ Hom_F = ( 𝑐 ∈ Cat ↦ ⟨ ( Hom_f ‘ 𝑐 ) , ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → 𝑐 = 𝐶 )
8	7	fveq2d	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( Hom_f ‘ 𝑐 ) = ( Hom_f ‘ 𝐶 ) )
9		fvexd	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( Base ‘ 𝑐 ) ∈ V )
10	7	fveq2d	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
11	10 3	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( Base ‘ 𝑐 ) = 𝐵 )
12		simpr	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
13	12	sqxpeqd	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) )
14		simplr	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → 𝑐 = 𝐶 )
15	14	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
16	15 4	eqtr4di	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑐 ) = 𝐻 )
17	16	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) )
18	16	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) = ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) )
19	16	fveq1d	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
20	14	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
21	20 5	eqtr4di	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( comp ‘ 𝑐 ) = · )
22	21	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) = ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) )
23	21	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) = ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) )
24	23	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) = ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) )
25		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → 𝑓 = 𝑓 )
26	22 24 25	oveq123d	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) = ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) )
27	19 26	mpteq12dv	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) = ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) )
28	17 18 27	mpoeq123dv	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) = ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) )
29	13 13 28	mpoeq123dv	⊢ ( ( ( 𝜑 ∧ 𝑐 = 𝐶 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) )
30	9 11 29	csbied2	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) )
31	8 30	opeq12d	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ⟨ ( Hom_f ‘ 𝑐 ) , ⦋ ( Base ‘ 𝑐 ) / 𝑏 ⦌ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ ( 𝑏 × 𝑏 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝑐 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝑐 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ = ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )
32		opex	⊢ ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ ∈ V
33	32	a1i	⊢ ( 𝜑 → ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ ∈ V )
34	6 31 2 33	fvmptd2	⊢ ( 𝜑 → ( Hom_F ‘ 𝐶 ) = ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )
35	1 34	syl5eq	⊢ ( 𝜑 → 𝑀 = ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ ( 𝐵 × 𝐵 ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) 𝐻 ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐻 ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( 𝐻 ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 · ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ · ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )

Metamath Proof Explorer

Theorem hofval

Proof