Theorem prf2

Description: Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	prfval.k	⊢ 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
	prfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	prfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	prfval.c	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	prfval.d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
	prf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	prf2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	prf2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion	prf2	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝑃 ) 𝑌 ) ‘ 𝐾 ) = ⟨ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		prfval.k	⊢ 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
2		prfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		prfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		prfval.c	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		prfval.d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
6		prf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		prf2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		prf2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
9	1 2 3 4 5 6 7	prf2fval	⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ 𝑃 ) 𝑌 ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ⟨ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) ⟩ ) )
10		simpr	⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ℎ = 𝐾 )
11	10	fveq2d	⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) = ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) )
12	10	fveq2d	⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) = ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) )
13	11 12	opeq12d	⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ⟨ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ ℎ ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ ℎ ) ⟩ = ⟨ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ )
14		opex	⊢ ⟨ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ ∈ V
15	14	a1i	⊢ ( 𝜑 → ⟨ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ ∈ V )
16	9 13 8 15	fvmptd	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝑃 ) 𝑌 ) ‘ 𝐾 ) = ⟨ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝐾 ) , ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) ⟩ )