catideu

Description: Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	catidex.b	$⊢ B = {Base}_{C}$
	catidex.h	$⊢ H = Hom (C)$
	catidex.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	catidex.c	$⊢ φ \to C \in Cat$
	catidex.x	$⊢ φ \to X \in B$
Assertion	catideu	$⊢ φ \to \exists! g \in (X H X) \forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f)$

Proof

Step	Hyp	Ref	Expression
1		catidex.b	$⊢ B = {Base}_{C}$
2		catidex.h	$⊢ H = Hom (C)$
3		catidex.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		catidex.c	$⊢ φ \to C \in Cat$
5		catidex.x	$⊢ φ \to X \in B$
6	1 2 3 4 5	catidex	$⊢ φ \to \exists g \in (X H X) \forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f)$
7		oveq1	$⊢ y = X \to y H X = X H X$
8		opeq1	$⊢ y = X \to ⟨y, X⟩ = ⟨X, X⟩$
9	8	oveq1d	$⊢ y = X \to ⟨y, X⟩ \underset{˙}{\cdot} X = ⟨X, X⟩ \underset{˙}{\cdot} X$
10	9	oveqd	$⊢ y = X \to g (⟨y, X⟩ \underset{˙}{\cdot} X) f = g (⟨X, X⟩ \underset{˙}{\cdot} X) f$
11	10	eqeq1d	$⊢ y = X \to (g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \leftrightarrow g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f)$
12	7 11	raleqbidv	$⊢ y = X \to (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \leftrightarrow \forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f)$
13		oveq2	$⊢ y = X \to X H y = X H X$
14		oveq2	$⊢ y = X \to ⟨X, X⟩ \underset{˙}{\cdot} y = ⟨X, X⟩ \underset{˙}{\cdot} X$
15	14	oveqd	$⊢ y = X \to f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f (⟨X, X⟩ \underset{˙}{\cdot} X) g$
16	15	eqeq1d	$⊢ y = X \to (f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f)$
17	13 16	raleqbidv	$⊢ y = X \to (\forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f)$
18	12 17	anbi12d	$⊢ y = X \to ((\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f) \leftrightarrow (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f))$
19	18	rspcv	$⊢ X \in B \to (\forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f) \to (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f))$
20	5 19	syl	$⊢ φ \to (\forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f) \to (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f))$
21	20	ralrimivw	$⊢ φ \to \forall g \in (X H X) (\forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f) \to (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f))$
22		an3	$⊢ ((\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f) \land (\forall f \in (X H X) h (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f)) \to (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f)$
23		oveq2	$⊢ f = h \to g (⟨X, X⟩ \underset{˙}{\cdot} X) f = g (⟨X, X⟩ \underset{˙}{\cdot} X) h$
24		id	$⊢ f = h \to f = h$
25	23 24	eqeq12d	$⊢ f = h \to (g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \leftrightarrow g (⟨X, X⟩ \underset{˙}{\cdot} X) h = h)$
26	25	rspcv	$⊢ h \in (X H X) \to (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \to g (⟨X, X⟩ \underset{˙}{\cdot} X) h = h)$
27		oveq1	$⊢ f = g \to f (⟨X, X⟩ \underset{˙}{\cdot} X) h = g (⟨X, X⟩ \underset{˙}{\cdot} X) h$
28		id	$⊢ f = g \to f = g$
29	27 28	eqeq12d	$⊢ f = g \to (f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f \leftrightarrow g (⟨X, X⟩ \underset{˙}{\cdot} X) h = g)$
30	29	rspcv	$⊢ g \in (X H X) \to (\forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f \to g (⟨X, X⟩ \underset{˙}{\cdot} X) h = g)$
31	26 30	im2anan9r	$⊢ (g \in (X H X) \land h \in (X H X)) \to ((\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f) \to (g (⟨X, X⟩ \underset{˙}{\cdot} X) h = h \land g (⟨X, X⟩ \underset{˙}{\cdot} X) h = g))$
32		eqtr2	$⊢ (g (⟨X, X⟩ \underset{˙}{\cdot} X) h = h \land g (⟨X, X⟩ \underset{˙}{\cdot} X) h = g) \to h = g$
33	32	equcomd	$⊢ (g (⟨X, X⟩ \underset{˙}{\cdot} X) h = h \land g (⟨X, X⟩ \underset{˙}{\cdot} X) h = g) \to g = h$
34	22 31 33	syl56	$⊢ (g \in (X H X) \land h \in (X H X)) \to (((\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f) \land (\forall f \in (X H X) h (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f)) \to g = h)$
35	34	rgen2	$⊢ \forall g \in (X H X) \forall h \in (X H X) (((\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f) \land (\forall f \in (X H X) h (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f)) \to g = h)$
36	35	a1i	$⊢ φ \to \forall g \in (X H X) \forall h \in (X H X) (((\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f) \land (\forall f \in (X H X) h (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f)) \to g = h)$
37		oveq1	$⊢ g = h \to g (⟨X, X⟩ \underset{˙}{\cdot} X) f = h (⟨X, X⟩ \underset{˙}{\cdot} X) f$
38	37	eqeq1d	$⊢ g = h \to (g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \leftrightarrow h (⟨X, X⟩ \underset{˙}{\cdot} X) f = f)$
39	38	ralbidv	$⊢ g = h \to (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \leftrightarrow \forall f \in (X H X) h (⟨X, X⟩ \underset{˙}{\cdot} X) f = f)$
40		oveq2	$⊢ g = h \to f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f (⟨X, X⟩ \underset{˙}{\cdot} X) h$
41	40	eqeq1d	$⊢ g = h \to (f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f \leftrightarrow f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f)$
42	41	ralbidv	$⊢ g = h \to (\forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f \leftrightarrow \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f)$
43	39 42	anbi12d	$⊢ g = h \to ((\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f) \leftrightarrow (\forall f \in (X H X) h (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f))$
44	43	rmo4	$⊢ \exists^{*} g \in (X H X) (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f) \leftrightarrow \forall g \in (X H X) \forall h \in (X H X) (((\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f) \land (\forall f \in (X H X) h (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) h = f)) \to g = h)$
45	36 44	sylibr	$⊢ φ \to \exists^{*} g \in (X H X) (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f)$
46		rmoim	$⊢ \forall g \in (X H X) (\forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f) \to (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f)) \to (\exists^{} g \in (X H X) (\forall f \in (X H X) g (⟨X, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H X) f (⟨X, X⟩ \underset{˙}{\cdot} X) g = f) \to \exists^{} g \in (X H X) \forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f))$
47	21 45 46	sylc	$⊢ φ \to \exists^{*} g \in (X H X) \forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f)$
48		reu5	$⊢ \exists! g \in (X H X) \forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f) \leftrightarrow (\exists g \in (X H X) \forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f) \land \exists^{*} g \in (X H X) \forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f))$
49	6 47 48	sylanbrc	$⊢ φ \to \exists! g \in (X H X) \forall y \in B (\forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f \land \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f)$

Metamath Proof Explorer

Theorem catideu

Proof