curfpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they curry the same functor to the same result. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Hypotheses	curfpropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
	curfpropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
	curfpropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	curfpropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
	curfpropd.a	$⊢ φ \to A \in Cat$
	curfpropd.b	$⊢ φ \to B \in Cat$
	curfpropd.c	$⊢ φ \to C \in Cat$
	curfpropd.d	$⊢ φ \to D \in Cat$
	curfpropd.f	$⊢ φ \to F \in ((A \times_{c} C) Func E)$
Assertion	curfpropd	$⊢ φ \to ⟨A, C⟩ {curry}_{F} F = ⟨B, D⟩ {curry}_{F} F$

Proof

Step	Hyp	Ref	Expression
1		curfpropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
2		curfpropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
3		curfpropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
4		curfpropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
5		curfpropd.a	$⊢ φ \to A \in Cat$
6		curfpropd.b	$⊢ φ \to B \in Cat$
7		curfpropd.c	$⊢ φ \to C \in Cat$
8		curfpropd.d	$⊢ φ \to D \in Cat$
9		curfpropd.f	$⊢ φ \to F \in ((A \times_{c} C) Func E)$
10	1	homfeqbas	$⊢ φ \to {Base}_{A} = {Base}_{B}$
11	3	homfeqbas	$⊢ φ \to {Base}_{C} = {Base}_{D}$
12	11	adantr	$⊢ (φ \land x \in {Base}_{A}) \to {Base}_{C} = {Base}_{D}$
13	12	mpteq1d	$⊢ (φ \land x \in {Base}_{A}) \to (y \in {Base}_{C} ⟼ x 1^{st} (F) y) = (y \in {Base}_{D} ⟼ x 1^{st} (F) y)$
14	12	adantr	$⊢ ((φ \land x \in {Base}_{A}) \land y \in {Base}_{C}) \to {Base}_{C} = {Base}_{D}$
15		eqid	$⊢ {Base}_{C} = {Base}_{C}$
16		eqid	$⊢ Hom (C) = Hom (C)$
17		eqid	$⊢ Hom (D) = Hom (D)$
18	3	ad2antrr	$⊢ ((φ \land x \in {Base}_{A}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
19		simprl	$⊢ ((φ \land x \in {Base}_{A}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to y \in {Base}_{C}$
20		simprr	$⊢ ((φ \land x \in {Base}_{A}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to z \in {Base}_{C}$
21	15 16 17 18 19 20	homfeqval	$⊢ ((φ \land x \in {Base}_{A}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to y Hom (C) z = y Hom (D) z$
22	1 2 5 6	cidpropd	$⊢ φ \to Id (A) = Id (B)$
23	22	ad2antrr	$⊢ ((φ \land x \in {Base}_{A}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to Id (A) = Id (B)$
24	23	fveq1d	$⊢ ((φ \land x \in {Base}_{A}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to Id (A) (x) = Id (B) (x)$
25	24	oveq1d	$⊢ ((φ \land x \in {Base}_{A}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to Id (A) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g = Id (B) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g$
26	21 25	mpteq12dv	$⊢ ((φ \land x \in {Base}_{A}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to (g \in (y Hom (C) z) ⟼ Id (A) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g) = (g \in (y Hom (D) z) ⟼ Id (B) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g)$
27	12 14 26	mpoeq123dva	$⊢ (φ \land x \in {Base}_{A}) \to (y \in {Base}_{C}, z \in {Base}_{C} ⟼ (g \in (y Hom (C) z) ⟼ Id (A) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g)) = (y \in {Base}_{D}, z \in {Base}_{D} ⟼ (g \in (y Hom (D) z) ⟼ Id (B) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))$
28	13 27	opeq12d	$⊢ (φ \land x \in {Base}_{A}) \to ⟨(y \in {Base}_{C} ⟼ x 1^{st} (F) y), (y \in {Base}_{C}, z \in {Base}_{C} ⟼ (g \in (y Hom (C) z) ⟼ Id (A) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩ = ⟨(y \in {Base}_{D} ⟼ x 1^{st} (F) y), (y \in {Base}_{D}, z \in {Base}_{D} ⟼ (g \in (y Hom (D) z) ⟼ Id (B) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩$
29	10 28	mpteq12dva	$⊢ φ \to (x \in {Base}_{A} ⟼ ⟨(y \in {Base}_{C} ⟼ x 1^{st} (F) y), (y \in {Base}_{C}, z \in {Base}_{C} ⟼ (g \in (y Hom (C) z) ⟼ Id (A) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩) = (x \in {Base}_{B} ⟼ ⟨(y \in {Base}_{D} ⟼ x 1^{st} (F) y), (y \in {Base}_{D}, z \in {Base}_{D} ⟼ (g \in (y Hom (D) z) ⟼ Id (B) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩)$
30	10	adantr	$⊢ (φ \land x \in {Base}_{A}) \to {Base}_{A} = {Base}_{B}$
31		eqid	$⊢ {Base}_{A} = {Base}_{A}$
32		eqid	$⊢ Hom (A) = Hom (A)$
33		eqid	$⊢ Hom (B) = Hom (B)$
34	1	adantr	$⊢ (φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
35		simprl	$⊢ (φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \to x \in {Base}_{A}$
36		simprr	$⊢ (φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \to y \in {Base}_{A}$
37	31 32 33 34 35 36	homfeqval	$⊢ (φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \to x Hom (A) y = x Hom (B) y$
38	11	ad2antrr	$⊢ ((φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \land g \in (x Hom (A) y)) \to {Base}_{C} = {Base}_{D}$
39	3 4 7 8	cidpropd	$⊢ φ \to Id (C) = Id (D)$
40	39	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \land g \in (x Hom (A) y)) \land z \in {Base}_{C}) \to Id (C) = Id (D)$
41	40	fveq1d	$⊢ (((φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \land g \in (x Hom (A) y)) \land z \in {Base}_{C}) \to Id (C) (z) = Id (D) (z)$
42	41	oveq2d	$⊢ (((φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \land g \in (x Hom (A) y)) \land z \in {Base}_{C}) \to g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (C) (z) = g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z)$
43	38 42	mpteq12dva	$⊢ ((φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \land g \in (x Hom (A) y)) \to (z \in {Base}_{C} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (C) (z)) = (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z))$
44	37 43	mpteq12dva	$⊢ (φ \land (x \in {Base}_{A} \land y \in {Base}_{A})) \to (g \in (x Hom (A) y) ⟼ (z \in {Base}_{C} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (C) (z))) = (g \in (x Hom (B) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z)))$
45	10 30 44	mpoeq123dva	$⊢ φ \to (x \in {Base}_{A}, y \in {Base}_{A} ⟼ (g \in (x Hom (A) y) ⟼ (z \in {Base}_{C} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (C) (z)))) = (x \in {Base}_{B}, y \in {Base}_{B} ⟼ (g \in (x Hom (B) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z))))$
46	29 45	opeq12d	$⊢ φ \to ⟨(x \in {Base}_{A} ⟼ ⟨(y \in {Base}_{C} ⟼ x 1^{st} (F) y), (y \in {Base}_{C}, z \in {Base}_{C} ⟼ (g \in (y Hom (C) z) ⟼ Id (A) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in {Base}_{A}, y \in {Base}_{A} ⟼ (g \in (x Hom (A) y) ⟼ (z \in {Base}_{C} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (C) (z))))⟩ = ⟨(x \in {Base}_{B} ⟼ ⟨(y \in {Base}_{D} ⟼ x 1^{st} (F) y), (y \in {Base}_{D}, z \in {Base}_{D} ⟼ (g \in (y Hom (D) z) ⟼ Id (B) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in {Base}_{B}, y \in {Base}_{B} ⟼ (g \in (x Hom (B) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z))))⟩$
47		eqid	$⊢ ⟨A, C⟩ {curry}_{F} F = ⟨A, C⟩ {curry}_{F} F$
48		eqid	$⊢ Id (A) = Id (A)$
49		eqid	$⊢ Id (C) = Id (C)$
50	47 31 5 7 9 15 16 48 32 49	curfval	$⊢ φ \to ⟨A, C⟩ {curry}_{F} F = ⟨(x \in {Base}_{A} ⟼ ⟨(y \in {Base}_{C} ⟼ x 1^{st} (F) y), (y \in {Base}_{C}, z \in {Base}_{C} ⟼ (g \in (y Hom (C) z) ⟼ Id (A) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in {Base}_{A}, y \in {Base}_{A} ⟼ (g \in (x Hom (A) y) ⟼ (z \in {Base}_{C} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (C) (z))))⟩$
51		eqid	$⊢ ⟨B, D⟩ {curry}_{F} F = ⟨B, D⟩ {curry}_{F} F$
52		eqid	$⊢ {Base}_{B} = {Base}_{B}$
53	1 2 3 4 5 6 7 8	xpcpropd	$⊢ φ \to A \times_{c} C = B \times_{c} D$
54	53	oveq1d	$⊢ φ \to (A \times_{c} C) Func E = (B \times_{c} D) Func E$
55	9 54	eleqtrd	$⊢ φ \to F \in ((B \times_{c} D) Func E)$
56		eqid	$⊢ {Base}_{D} = {Base}_{D}$
57		eqid	$⊢ Id (B) = Id (B)$
58		eqid	$⊢ Id (D) = Id (D)$
59	51 52 6 8 55 56 17 57 33 58	curfval	$⊢ φ \to ⟨B, D⟩ {curry}_{F} F = ⟨(x \in {Base}_{B} ⟼ ⟨(y \in {Base}_{D} ⟼ x 1^{st} (F) y), (y \in {Base}_{D}, z \in {Base}_{D} ⟼ (g \in (y Hom (D) z) ⟼ Id (B) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in {Base}_{B}, y \in {Base}_{B} ⟼ (g \in (x Hom (B) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z))))⟩$
60	46 50 59	3eqtr4d	$⊢ φ \to ⟨A, C⟩ {curry}_{F} F = ⟨B, D⟩ {curry}_{F} F$

Metamath Proof Explorer

Theorem curfpropd

Proof