oppccomfpropd

Description: If two categories have the same hom-sets and composition, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Hypotheses	oppchomfpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	oppccomfpropd.1	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
Assertion	oppccomfpropd	$⊢ φ \to {comp}_{𝑓} (oppCat (C)) = {comp}_{𝑓} (oppCat (D))$

Proof

Step	Hyp	Ref	Expression
1		oppchomfpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
2		oppccomfpropd.1	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
3		eqid	$⊢ {Base}_{C} = {Base}_{C}$
4		eqid	$⊢ Hom (C) = Hom (C)$
5		eqid	$⊢ comp (C) = comp (C)$
6		eqid	$⊢ comp (D) = comp (D)$
7	1	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
8	2	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
9		simplr3	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to z \in {Base}_{C}$
10		simplr2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to y \in {Base}_{C}$
11		simplr1	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to x \in {Base}_{C}$
12		simprr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to g \in (y Hom (oppCat (C)) z)$
13		eqid	$⊢ oppCat (C) = oppCat (C)$
14	4 13	oppchom	$⊢ y Hom (oppCat (C)) z = z Hom (C) y$
15	12 14	eleqtrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to g \in (z Hom (C) y)$
16		simprl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to f \in (x Hom (oppCat (C)) y)$
17	4 13	oppchom	$⊢ x Hom (oppCat (C)) y = y Hom (C) x$
18	16 17	eleqtrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to f \in (y Hom (C) x)$
19	3 4 5 6 7 8 9 10 11 15 18	comfeqval	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to f (⟨z, y⟩ comp (C) x) g = f (⟨z, y⟩ comp (D) x) g$
20	3 5 13 11 10 9	oppcco	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to g (⟨x, y⟩ comp (oppCat (C)) z) f = f (⟨z, y⟩ comp (C) x) g$
21		eqid	$⊢ {Base}_{D} = {Base}_{D}$
22		eqid	$⊢ oppCat (D) = oppCat (D)$
23	1	homfeqbas	$⊢ φ \to {Base}_{C} = {Base}_{D}$
24	23	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to {Base}_{C} = {Base}_{D}$
25	11 24	eleqtrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to x \in {Base}_{D}$
26	10 24	eleqtrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to y \in {Base}_{D}$
27	9 24	eleqtrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to z \in {Base}_{D}$
28	21 6 22 25 26 27	oppcco	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to g (⟨x, y⟩ comp (oppCat (D)) z) f = f (⟨z, y⟩ comp (D) x) g$
29	19 20 28	3eqtr4d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \land (f \in (x Hom (oppCat (C)) y) \land g \in (y Hom (oppCat (C)) z))) \to g (⟨x, y⟩ comp (oppCat (C)) z) f = g (⟨x, y⟩ comp (oppCat (D)) z) f$
30	29	ralrimivva	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C})) \to \forall f \in (x Hom (oppCat (C)) y) \forall g \in (y Hom (oppCat (C)) z) g (⟨x, y⟩ comp (oppCat (C)) z) f = g (⟨x, y⟩ comp (oppCat (D)) z) f$
31	30	ralrimivvva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (oppCat (C)) y) \forall g \in (y Hom (oppCat (C)) z) g (⟨x, y⟩ comp (oppCat (C)) z) f = g (⟨x, y⟩ comp (oppCat (D)) z) f$
32		eqid	$⊢ comp (oppCat (C)) = comp (oppCat (C))$
33		eqid	$⊢ comp (oppCat (D)) = comp (oppCat (D))$
34		eqid	$⊢ Hom (oppCat (C)) = Hom (oppCat (C))$
35	13 3	oppcbas	$⊢ {Base}_{C} = {Base}_{oppCat (C)}$
36	35	a1i	$⊢ φ \to {Base}_{C} = {Base}_{oppCat (C)}$
37	22 21	oppcbas	$⊢ {Base}_{D} = {Base}_{oppCat (D)}$
38	23 37	eqtrdi	$⊢ φ \to {Base}_{C} = {Base}_{oppCat (D)}$
39	1	oppchomfpropd	$⊢ φ \to {Hom}_{𝑓} (oppCat (C)) = {Hom}_{𝑓} (oppCat (D))$
40	32 33 34 36 38 39	comfeq	$⊢ φ \to ({comp}_{𝑓} (oppCat (C)) = {comp}_{𝑓} (oppCat (D)) \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (oppCat (C)) y) \forall g \in (y Hom (oppCat (C)) z) g (⟨x, y⟩ comp (oppCat (C)) z) f = g (⟨x, y⟩ comp (oppCat (D)) z) f)$
41	31 40	mpbird	$⊢ φ \to {comp}_{𝑓} (oppCat (C)) = {comp}_{𝑓} (oppCat (D))$

Metamath Proof Explorer

Theorem oppccomfpropd

Proof