curf1

Description: Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
	curfval.a	$⊢ A = {Base}_{C}$
	curfval.c	$⊢ φ \to C \in Cat$
	curfval.d	$⊢ φ \to D \in Cat$
	curfval.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
	curfval.b	$⊢ B = {Base}_{D}$
	curf1.x	$⊢ φ \to X \in A$
	curf1.k	$⊢ K = 1^{st} (G) (X)$
	curf1.j	$⊢ J = Hom (D)$
	curf1.1	$⊢ \underset{˙}{1} = Id (C)$
Assertion	curf1	$⊢ φ \to K = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩$

Proof

Step	Hyp	Ref	Expression
1		curfval.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
2		curfval.a	$⊢ A = {Base}_{C}$
3		curfval.c	$⊢ φ \to C \in Cat$
4		curfval.d	$⊢ φ \to D \in Cat$
5		curfval.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
6		curfval.b	$⊢ B = {Base}_{D}$
7		curf1.x	$⊢ φ \to X \in A$
8		curf1.k	$⊢ K = 1^{st} (G) (X)$
9		curf1.j	$⊢ J = Hom (D)$
10		curf1.1	$⊢ \underset{˙}{1} = Id (C)$
11	1 2 3 4 5 6 9 10	curf1fval	$⊢ φ \to 1^{st} (G) = (x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩)$
12		simpr	$⊢ (φ \land x = X) \to x = X$
13	12	oveq1d	$⊢ (φ \land x = X) \to x 1^{st} (F) y = X 1^{st} (F) y$
14	13	mpteq2dv	$⊢ (φ \land x = X) \to (y \in B ⟼ x 1^{st} (F) y) = (y \in B ⟼ X 1^{st} (F) y)$
15		simp1r	$⊢ ((φ \land x = X) \land y \in B \land z \in B) \to x = X$
16	15	opeq1d	$⊢ ((φ \land x = X) \land y \in B \land z \in B) \to ⟨x, y⟩ = ⟨X, y⟩$
17	15	opeq1d	$⊢ ((φ \land x = X) \land y \in B \land z \in B) \to ⟨x, z⟩ = ⟨X, z⟩$
18	16 17	oveq12d	$⊢ ((φ \land x = X) \land y \in B \land z \in B) \to ⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩ = ⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩$
19	15	fveq2d	$⊢ ((φ \land x = X) \land y \in B \land z \in B) \to \underset{˙}{1} (x) = \underset{˙}{1} (X)$
20		eqidd	$⊢ ((φ \land x = X) \land y \in B \land z \in B) \to g = g$
21	18 19 20	oveq123d	$⊢ ((φ \land x = X) \land y \in B \land z \in B) \to \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g = \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g$
22	21	mpteq2dv	$⊢ ((φ \land x = X) \land y \in B \land z \in B) \to (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g) = (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g)$
23	22	mpoeq3dva	$⊢ (φ \land x = X) \to (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g)) = (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))$
24	14 23	opeq12d	$⊢ (φ \land x = X) \to ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩ = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩$
25		opex	$⊢ ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩ \in V$
26	25	a1i	$⊢ φ \to ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩ \in V$
27	11 24 7 26	fvmptd	$⊢ φ \to 1^{st} (G) (X) = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩$
28	8 27	syl5eq	$⊢ φ \to K = ⟨(y \in B ⟼ X 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (X) (⟨X, y⟩ 2^{nd} (F) ⟨X, z⟩) g))⟩$

Metamath Proof Explorer

Theorem curf1

Proof