hof1fval

Description: The object part of the Hom functor is the Homf operation, which is just a functionalized version of Hom . That is, it is a two argument function, which maps X , Y to the set of morphisms from X to Y . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	⊢ 𝑀 = ( Hom_F ‘ 𝐶 )
	hofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion	hof1fval	⊢ ( 𝜑 → ( 1^st ‘ 𝑀 ) = ( Hom_f ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		hofval.m	⊢ 𝑀 = ( Hom_F ‘ 𝐶 )
2		hofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
4		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
5		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
6	1 2 3 4 5	hofval	⊢ ( 𝜑 → 𝑀 = ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )
7		fvex	⊢ ( Hom_f ‘ 𝐶 ) ∈ V
8		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
9	8 8	xpex	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ V
10	9 9	mpoex	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ∈ V
11	7 10	op1std	⊢ ( 𝑀 = ⟨ ( Hom_f ‘ 𝐶 ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↦ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ → ( 1^st ‘ 𝑀 ) = ( Hom_f ‘ 𝐶 ) )
12	6 11	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑀 ) = ( Hom_f ‘ 𝐶 ) )

Metamath Proof Explorer

Theorem hof1fval

Proof