curf2

Description: Value of the curry functor at a morphism. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	curf2.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
	curf2.a	$⊢ A = {Base}_{C}$
	curf2.c	$⊢ φ \to C \in Cat$
	curf2.d	$⊢ φ \to D \in Cat$
	curf2.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
	curf2.b	$⊢ B = {Base}_{D}$
	curf2.h	$⊢ H = Hom (C)$
	curf2.i	$⊢ I = Id (D)$
	curf2.x	$⊢ φ \to X \in A$
	curf2.y	$⊢ φ \to Y \in A$
	curf2.k	$⊢ φ \to K \in (X H Y)$
	curf2.l	$⊢ L = (X 2^{nd} (G) Y) (K)$
Assertion	curf2	$⊢ φ \to L = (z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z))$

Proof

Step	Hyp	Ref	Expression
1		curf2.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
2		curf2.a	$⊢ A = {Base}_{C}$
3		curf2.c	$⊢ φ \to C \in Cat$
4		curf2.d	$⊢ φ \to D \in Cat$
5		curf2.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
6		curf2.b	$⊢ B = {Base}_{D}$
7		curf2.h	$⊢ H = Hom (C)$
8		curf2.i	$⊢ I = Id (D)$
9		curf2.x	$⊢ φ \to X \in A$
10		curf2.y	$⊢ φ \to Y \in A$
11		curf2.k	$⊢ φ \to K \in (X H Y)$
12		curf2.l	$⊢ L = (X 2^{nd} (G) Y) (K)$
13		eqid	$⊢ Hom (D) = Hom (D)$
14		eqid	$⊢ Id (C) = Id (C)$
15	1 2 3 4 5 6 13 14 7 8	curfval	$⊢ φ \to G = ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩$
16	2	fvexi	$⊢ A \in V$
17	16	mptex	$⊢ (x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩) \in V$
18	16 16	mpoex	$⊢ (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z)))) \in V$
19	17 18	op2ndd	$⊢ G = ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩ \to 2^{nd} (G) = (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))$
20	15 19	syl	$⊢ φ \to 2^{nd} (G) = (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))$
21	10	adantr	$⊢ (φ \land x = X) \to Y \in A$
22		ovex	$⊢ x H y \in V$
23	22	mptex	$⊢ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))) \in V$
24	23	a1i	$⊢ (φ \land (x = X \land y = Y)) \to (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))) \in V$
25	11	adantr	$⊢ (φ \land (x = X \land y = Y)) \to K \in (X H Y)$
26		simprl	$⊢ (φ \land (x = X \land y = Y)) \to x = X$
27		simprr	$⊢ (φ \land (x = X \land y = Y)) \to y = Y$
28	26 27	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x H y = X H Y$
29	25 28	eleqtrrd	$⊢ (φ \land (x = X \land y = Y)) \to K \in (x H y)$
30	6	fvexi	$⊢ B \in V$
31	30	mptex	$⊢ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z)) \in V$
32	31	a1i	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z)) \in V$
33		simplrl	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to x = X$
34	33	opeq1d	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to ⟨x, z⟩ = ⟨X, z⟩$
35		simplrr	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to y = Y$
36	35	opeq1d	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to ⟨y, z⟩ = ⟨Y, z⟩$
37	34 36	oveq12d	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to ⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩ = ⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩$
38		simpr	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to g = K$
39		eqidd	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to I (z) = I (z)$
40	37 38 39	oveq123d	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z) = K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z)$
41	40	mpteq2dv	$⊢ ((φ \land (x = X \land y = Y)) \land g = K) \to (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z)) = (z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z))$
42	29 32 41	fvmptdv2	$⊢ (φ \land (x = X \land y = Y)) \to (X 2^{nd} (G) Y = (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))) \to (X 2^{nd} (G) Y) (K) = (z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z)))$
43	9 21 24 42	ovmpodv	$⊢ φ \to (2^{nd} (G) = (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z)))) \to (X 2^{nd} (G) Y) (K) = (z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z)))$
44	20 43	mpd	$⊢ φ \to (X 2^{nd} (G) Y) (K) = (z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z))$
45	12 44	syl5eq	$⊢ φ \to L = (z \in B ⟼ K (⟨X, z⟩ 2^{nd} (F) ⟨Y, z⟩) I (z))$

Metamath Proof Explorer

Theorem curf2

Proof