prf2fval

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

	Ref	Expression
Hypotheses	prfval.k	$⊢ P = F {⟨,⟩}_{F} G$
	prfval.b	$⊢ B = {Base}_{C}$
	prfval.h	$⊢ H = Hom (C)$
	prfval.c	$⊢ φ \to F \in (C Func D)$
	prfval.d	$⊢ φ \to G \in (C Func E)$
	prf1.x	$⊢ φ \to X \in B$
	prf2.y	$⊢ φ \to Y \in B$
Assertion	prf2fval	$⊢ φ \to X 2^{nd} (P) Y = (h \in (X H Y) ⟼ ⟨(X 2^{nd} (F) Y) (h), (X 2^{nd} (G) Y) (h)⟩)$

Proof

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	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)⟩))⟩$
9	2	fvexi	$⊢ B \in V$
10	9	mptex	$⊢ (x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩) \in V$
11	9 9	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$
12	10 11	op2ndd	$⊢ 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 2^{nd} (P) = (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))$
13	8 12	syl	$⊢ φ \to 2^{nd} (P) = (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))$
14		simprl	$⊢ (φ \land (x = X \land y = Y)) \to x = X$
15		simprr	$⊢ (φ \land (x = X \land y = Y)) \to y = Y$
16	14 15	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x H y = X H Y$
17	14 15	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x 2^{nd} (F) y = X 2^{nd} (F) Y$
18	17	fveq1d	$⊢ (φ \land (x = X \land y = Y)) \to (x 2^{nd} (F) y) (h) = (X 2^{nd} (F) Y) (h)$
19	14 15	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x 2^{nd} (G) y = X 2^{nd} (G) Y$
20	19	fveq1d	$⊢ (φ \land (x = X \land y = Y)) \to (x 2^{nd} (G) y) (h) = (X 2^{nd} (G) Y) (h)$
21	18 20	opeq12d	$⊢ (φ \land (x = X \land y = Y)) \to ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩ = ⟨(X 2^{nd} (F) Y) (h), (X 2^{nd} (G) Y) (h)⟩$
22	16 21	mpteq12dv	$⊢ (φ \land (x = X \land y = Y)) \to (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩) = (h \in (X H Y) ⟼ ⟨(X 2^{nd} (F) Y) (h), (X 2^{nd} (G) Y) (h)⟩)$
23		ovex	$⊢ X H Y \in V$
24	23	mptex	$⊢ (h \in (X H Y) ⟼ ⟨(X 2^{nd} (F) Y) (h), (X 2^{nd} (G) Y) (h)⟩) \in V$
25	24	a1i	$⊢ φ \to (h \in (X H Y) ⟼ ⟨(X 2^{nd} (F) Y) (h), (X 2^{nd} (G) Y) (h)⟩) \in V$
26	13 22 6 7 25	ovmpod	$⊢ φ \to X 2^{nd} (P) Y = (h \in (X H Y) ⟼ ⟨(X 2^{nd} (F) Y) (h), (X 2^{nd} (G) Y) (h)⟩)$

Metamath Proof Explorer

Theorem prf2fval

Proof