Theorem comffval2

Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	comfffval2.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
	comfffval2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	comfffval2.h	⊢ 𝐻 = ( Homf ‘ 𝐶 )
	comfffval2.x	⊢ · = ( comp ‘ 𝐶 )
	comffval2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	comffval2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	comffval2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	comffval2	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		comfffval2.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
2		comfffval2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		comfffval2.h	⊢ 𝐻 = ( Homf ‘ 𝐶 )
4		comfffval2.x	⊢ · = ( comp ‘ 𝐶 )
5		comffval2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		comffval2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		comffval2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9	1 2 8 4 5 6 7	comffval	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) = ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) , 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) )
10	3 2 8 6 7	homfval	⊢ ( 𝜑 → ( 𝑌 𝐻 𝑍 ) = ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
11	3 2 8 5 6	homfval	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
12		eqidd	⊢ ( 𝜑 → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) )
13	10 11 12	mpoeq123dv	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) = ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) , 𝑓 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) )
14	9 13	eqtr4d	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝑓 ) ) )