catidex

Description: Each object in a category has an associated 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	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)$

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		id	$⊢ x = X \to x = X$
7	6 6	oveq12d	$⊢ x = X \to x H x = X H X$
8		oveq2	$⊢ x = X \to y H x = y H X$
9		opeq2	$⊢ x = X \to ⟨y, x⟩ = ⟨y, X⟩$
10	9 6	oveq12d	$⊢ x = X \to ⟨y, x⟩ \underset{˙}{\cdot} x = ⟨y, X⟩ \underset{˙}{\cdot} X$
11	10	oveqd	$⊢ x = X \to g (⟨y, x⟩ \underset{˙}{\cdot} x) f = g (⟨y, X⟩ \underset{˙}{\cdot} X) f$
12	11	eqeq1d	$⊢ x = X \to (g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \leftrightarrow g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f)$
13	8 12	raleqbidv	$⊢ x = X \to (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \leftrightarrow \forall f \in (y H X) g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f)$
14		oveq1	$⊢ x = X \to x H y = X H y$
15	6 6	opeq12d	$⊢ x = X \to ⟨x, x⟩ = ⟨X, X⟩$
16	15	oveq1d	$⊢ x = X \to ⟨x, x⟩ \underset{˙}{\cdot} y = ⟨X, X⟩ \underset{˙}{\cdot} y$
17	16	oveqd	$⊢ x = X \to f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f (⟨X, X⟩ \underset{˙}{\cdot} y) g$
18	17	eqeq1d	$⊢ x = X \to (f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f)$
19	14 18	raleqbidv	$⊢ x = X \to (\forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f)$
20	13 19	anbi12d	$⊢ x = 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 (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))$
21	20	ralbidv	$⊢ x = X \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) \leftrightarrow \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))$
22	7 21	rexeqbidv	$⊢ x = X \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) \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))$
23	1 2 3	iscat	$⊢ C \in Cat \to (C \in Cat \leftrightarrow \forall x \in B (\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 \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))))$
24	23	ibi	$⊢ C \in Cat \to \forall x \in B (\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 \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)))$
25		simpl	$⊢ (\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 \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) 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)$
26	25	ralimi	$⊢ \forall x \in B (\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 \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))) \to \forall x \in B \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)$
27	4 24 26	3syl	$⊢ φ \to \forall x \in B \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)$
28	22 27 5	rspcdva	$⊢ φ \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 catidex

Proof