oppccatid

		Ref	Expression
	Hypothesis	oppcbas.1	$⊢ O = oppCat (C)$
	Assertion	oppccatid	$⊢ C \in Cat \to (O \in Cat \land Id (O) = Id (C))$

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	$⊢ O = oppCat (C)$
2		eqid	$⊢ {Base}_{C} = {Base}_{C}$
3	1 2	oppcbas	$⊢ {Base}_{C} = {Base}_{O}$
4	3	a1i	$⊢ C \in Cat \to {Base}_{C} = {Base}_{O}$
5		eqidd	$⊢ C \in Cat \to Hom (O) = Hom (O)$
6		eqidd	$⊢ C \in Cat \to comp (O) = comp (O)$
7	1	fvexi	$⊢ O \in V$
8	7	a1i	$⊢ C \in Cat \to O \in V$
9		biid	$⊢ ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w))) \leftrightarrow ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))$
10		eqid	$⊢ Hom (C) = Hom (C)$
11		eqid	$⊢ Id (C) = Id (C)$
12		simpl	$⊢ (C \in Cat \land y \in {Base}_{C}) \to C \in Cat$
13		simpr	$⊢ (C \in Cat \land y \in {Base}_{C}) \to y \in {Base}_{C}$
14	2 10 11 12 13	catidcl	$⊢ (C \in Cat \land y \in {Base}_{C}) \to Id (C) (y) \in (y Hom (C) y)$
15	10 1	oppchom	$⊢ y Hom (O) y = y Hom (C) y$
16	14 15	eleqtrrdi	$⊢ (C \in Cat \land y \in {Base}_{C}) \to Id (C) (y) \in (y Hom (O) y)$
17		eqid	$⊢ comp (C) = comp (C)$
18		simpr1l	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to x \in {Base}_{C}$
19		simpr1r	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to y \in {Base}_{C}$
20	2 17 1 18 19 19	oppcco	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to Id (C) (y) (⟨x, y⟩ comp (O) y) f = f (⟨y, y⟩ comp (C) x) Id (C) (y)$
21		simpl	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to C \in Cat$
22		simpr31	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to f \in (x Hom (O) y)$
23	10 1	oppchom	$⊢ x Hom (O) y = y Hom (C) x$
24	22 23	eleqtrdi	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to f \in (y Hom (C) x)$
25	2 10 11 21 19 17 18 24	catrid	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to f (⟨y, y⟩ comp (C) x) Id (C) (y) = f$
26	20 25	eqtrd	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to Id (C) (y) (⟨x, y⟩ comp (O) y) f = f$
27		simpr2l	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to z \in {Base}_{C}$
28	2 17 1 19 19 27	oppcco	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to g (⟨y, y⟩ comp (O) z) Id (C) (y) = Id (C) (y) (⟨z, y⟩ comp (C) y) g$
29		simpr32	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to g \in (y Hom (O) z)$
30	10 1	oppchom	$⊢ y Hom (O) z = z Hom (C) y$
31	29 30	eleqtrdi	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to g \in (z Hom (C) y)$
32	2 10 11 21 27 17 19 31	catlid	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to Id (C) (y) (⟨z, y⟩ comp (C) y) g = g$
33	28 32	eqtrd	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to g (⟨y, y⟩ comp (O) z) Id (C) (y) = g$
34	2 17 1 18 19 27	oppcco	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to g (⟨x, y⟩ comp (O) z) f = f (⟨z, y⟩ comp (C) x) g$
35	2 10 17 21 27 19 18 31 24	catcocl	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to f (⟨z, y⟩ comp (C) x) g \in (z Hom (C) x)$
36	34 35	eqeltrd	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to g (⟨x, y⟩ comp (O) z) f \in (z Hom (C) x)$
37	10 1	oppchom	$⊢ x Hom (O) z = z Hom (C) x$
38	36 37	eleqtrrdi	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to g (⟨x, y⟩ comp (O) z) f \in (x Hom (O) z)$
39		simpr2r	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to w \in {Base}_{C}$
40		simpr33	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to h \in (z Hom (O) w)$
41	10 1	oppchom	$⊢ z Hom (O) w = w Hom (C) z$
42	40 41	eleqtrdi	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to h \in (w Hom (C) z)$
43	2 10 17 21 39 27 19 42 31 18 24	catass	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to (f (⟨z, y⟩ comp (C) x) g) (⟨w, z⟩ comp (C) x) h = f (⟨w, y⟩ comp (C) x) (g (⟨w, z⟩ comp (C) y) h)$
44	2 17 1 18 27 39	oppcco	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to h (⟨x, z⟩ comp (O) w) (f (⟨z, y⟩ comp (C) x) g) = (f (⟨z, y⟩ comp (C) x) g) (⟨w, z⟩ comp (C) x) h$
45	2 17 1 18 19 39	oppcco	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to (g (⟨w, z⟩ comp (C) y) h) (⟨x, y⟩ comp (O) w) f = f (⟨w, y⟩ comp (C) x) (g (⟨w, z⟩ comp (C) y) h)$
46	43 44 45	3eqtr4rd	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to (g (⟨w, z⟩ comp (C) y) h) (⟨x, y⟩ comp (O) w) f = h (⟨x, z⟩ comp (O) w) (f (⟨z, y⟩ comp (C) x) g)$
47	2 17 1 19 27 39	oppcco	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to h (⟨y, z⟩ comp (O) w) g = g (⟨w, z⟩ comp (C) y) h$
48	47	oveq1d	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to (h (⟨y, z⟩ comp (O) w) g) (⟨x, y⟩ comp (O) w) f = (g (⟨w, z⟩ comp (C) y) h) (⟨x, y⟩ comp (O) w) f$
49	34	oveq2d	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to h (⟨x, z⟩ comp (O) w) (g (⟨x, y⟩ comp (O) z) f) = h (⟨x, z⟩ comp (O) w) (f (⟨z, y⟩ comp (C) x) g)$
50	46 48 49	3eqtr4d	$⊢ (C \in Cat \land ((x \in {Base}_{C} \land y \in {Base}_{C}) \land (z \in {Base}_{C} \land w \in {Base}_{C}) \land (f \in (x Hom (O) y) \land g \in (y Hom (O) z) \land h \in (z Hom (O) w)))) \to (h (⟨y, z⟩ comp (O) w) g) (⟨x, y⟩ comp (O) w) f = h (⟨x, z⟩ comp (O) w) (g (⟨x, y⟩ comp (O) z) f)$
51	4 5 6 8 9 16 26 33 38 50	iscatd2	$⊢ C \in Cat \to (O \in Cat \land Id (O) = (y \in {Base}_{C} ⟼ Id (C) (y)))$
52	2 11	cidfn	$⊢ C \in Cat \to Id (C) Fn {Base}_{C}$
53		dffn5	$⊢ Id (C) Fn {Base}_{C} \leftrightarrow Id (C) = (y \in {Base}_{C} ⟼ Id (C) (y))$
54	52 53	sylib	$⊢ C \in Cat \to Id (C) = (y \in {Base}_{C} ⟼ Id (C) (y))$
55	54	eqeq2d	$⊢ C \in Cat \to (Id (O) = Id (C) \leftrightarrow Id (O) = (y \in {Base}_{C} ⟼ Id (C) (y)))$
56	55	anbi2d	$⊢ C \in Cat \to ((O \in Cat \land Id (O) = Id (C)) \leftrightarrow (O \in Cat \land Id (O) = (y \in {Base}_{C} ⟼ Id (C) (y))))$
57	51 56	mpbird	$⊢ C \in Cat \to (O \in Cat \land Id (O) = Id (C))$

Metamath Proof Explorer

Theorem oppccatid

Proof