prf1

Description: Value of the pairing functor on objects. (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	1 2 3 4 5	prfval	$⊢ φ \to P = ⟨(x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩$
8	2	fvexi	$⊢ B \in V$
9	8	mptex	$⊢ (x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩) \in V$
10	8 8	mpoex	$⊢ (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩)) \in V$
11	9 10	op1std	$⊢ P = ⟨(x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩ \to 1^{st} (P) = (x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩)$
12	7 11	syl	$⊢ φ \to 1^{st} (P) = (x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩)$
13		simpr	$⊢ (φ \land x = X) \to x = X$
14	13	fveq2d	$⊢ (φ \land x = X) \to 1^{st} (F) (x) = 1^{st} (F) (X)$
15	13	fveq2d	$⊢ (φ \land x = X) \to 1^{st} (G) (x) = 1^{st} (G) (X)$
16	14 15	opeq12d	$⊢ (φ \land x = X) \to ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ = ⟨1^{st} (F) (X), 1^{st} (G) (X)⟩$
17		opex	$⊢ ⟨1^{st} (F) (X), 1^{st} (G) (X)⟩ \in V$
18	17	a1i	$⊢ φ \to ⟨1^{st} (F) (X), 1^{st} (G) (X)⟩ \in V$
19	12 16 6 18	fvmptd	$⊢ φ \to 1^{st} (P) (X) = ⟨1^{st} (F) (X), 1^{st} (G) (X)⟩$

Metamath Proof Explorer