prf2

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

Step	Hyp	Ref	Expression
1		prfval.k	$⊢ P = F {⟨,⟩}_{F} G$
2		prfval.b	$⊢ B = {Base}_{C}$
3		prfval.h	$⊢ H = Hom (C)$
4		prfval.c	$⊢ φ \to F \in (C Func D)$
5		prfval.d	$⊢ φ \to G \in (C Func E)$
6		prf1.x	$⊢ φ \to X \in B$
7		prf2.y	$⊢ φ \to Y \in B$
8		prf2.k	$⊢ φ \to K \in (X H Y)$
9	1 2 3 4 5 6 7	prf2fval	$⊢ φ \to X 2^{nd} (P) Y = (h \in (X H Y) ⟼ ⟨(X 2^{nd} (F) Y) (h), (X 2^{nd} (G) Y) (h)⟩)$
10		simpr	$⊢ (φ \land h = K) \to h = K$
11	10	fveq2d	$⊢ (φ \land h = K) \to (X 2^{nd} (F) Y) (h) = (X 2^{nd} (F) Y) (K)$
12	10	fveq2d	$⊢ (φ \land h = K) \to (X 2^{nd} (G) Y) (h) = (X 2^{nd} (G) Y) (K)$
13	11 12	opeq12d	$⊢ (φ \land h = K) \to ⟨(X 2^{nd} (F) Y) (h), (X 2^{nd} (G) Y) (h)⟩ = ⟨(X 2^{nd} (F) Y) (K), (X 2^{nd} (G) Y) (K)⟩$
14		opex	$⊢ ⟨(X 2^{nd} (F) Y) (K), (X 2^{nd} (G) Y) (K)⟩ \in V$
15	14	a1i	$⊢ φ \to ⟨(X 2^{nd} (F) Y) (K), (X 2^{nd} (G) Y) (K)⟩ \in V$
16	9 13 8 15	fvmptd	$⊢ φ \to (X 2^{nd} (P) Y) (K) = ⟨(X 2^{nd} (F) Y) (K), (X 2^{nd} (G) Y) (K)⟩$

Metamath Proof Explorer