catidd

Description: Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	catidd.b	$⊢ φ \to B = {Base}_{C}$
	catidd.h	$⊢ φ \to H = Hom (C)$
	catidd.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
	catidd.c	$⊢ φ \to C \in Cat$
	catidd.1	$⊢ (φ \land x \in B) \to \underset{˙}{1} \in (x H x)$
	catidd.2	$⊢ (φ \land (x \in B \land y \in B \land f \in (y H x))) \to \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f$
	catidd.3	$⊢ (φ \land (x \in B \land y \in B \land f \in (x H y))) \to f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f$
Assertion	catidd	$⊢ φ \to Id (C) = (x \in B ⟼ \underset{˙}{1})$

Proof

Step	Hyp	Ref	Expression
1		catidd.b	$⊢ φ \to B = {Base}_{C}$
2		catidd.h	$⊢ φ \to H = Hom (C)$
3		catidd.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
4		catidd.c	$⊢ φ \to C \in Cat$
5		catidd.1	$⊢ (φ \land x \in B) \to \underset{˙}{1} \in (x H x)$
6		catidd.2	$⊢ (φ \land (x \in B \land y \in B \land f \in (y H x))) \to \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f$
7		catidd.3	$⊢ (φ \land (x \in B \land y \in B \land f \in (x H y))) \to f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f$
8	6	ex	$⊢ φ \to ((x \in B \land y \in B \land f \in (y H x)) \to \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f)$
9	1	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in {Base}_{C})$
10	1	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in {Base}_{C})$
11	2	oveqd	$⊢ φ \to y H x = y Hom (C) x$
12	11	eleq2d	$⊢ φ \to (f \in (y H x) \leftrightarrow f \in (y Hom (C) x))$
13	9 10 12	3anbi123d	$⊢ φ \to ((x \in B \land y \in B \land f \in (y H x)) \leftrightarrow (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (y Hom (C) x)))$
14	3	oveqd	$⊢ φ \to ⟨y, x⟩ \underset{˙}{\cdot} x = ⟨y, x⟩ comp (C) x$
15	14	oveqd	$⊢ φ \to \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (⟨y, x⟩ comp (C) x) f$
16	15	eqeq1d	$⊢ φ \to (\underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \leftrightarrow \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f)$
17	8 13 16	3imtr3d	$⊢ φ \to ((x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (y Hom (C) x)) \to \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f)$
18	17	3expd	$⊢ φ \to (x \in {Base}_{C} \to (y \in {Base}_{C} \to (f \in (y Hom (C) x) \to \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f)))$
19	18	imp41	$⊢ (((φ \land x \in {Base}_{C}) \land y \in {Base}_{C}) \land f \in (y Hom (C) x)) \to \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f$
20	19	ralrimiva	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{C}) \to \forall f \in (y Hom (C) x) \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f$
21	7	ex	$⊢ φ \to ((x \in B \land y \in B \land f \in (x H y)) \to f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f)$
22	2	oveqd	$⊢ φ \to x H y = x Hom (C) y$
23	22	eleq2d	$⊢ φ \to (f \in (x H y) \leftrightarrow f \in (x Hom (C) y))$
24	9 10 23	3anbi123d	$⊢ φ \to ((x \in B \land y \in B \land f \in (x H y)) \leftrightarrow (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y)))$
25	3	oveqd	$⊢ φ \to ⟨x, x⟩ \underset{˙}{\cdot} y = ⟨x, x⟩ comp (C) y$
26	25	oveqd	$⊢ φ \to f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f (⟨x, x⟩ comp (C) y) \underset{˙}{1}$
27	26	eqeq1d	$⊢ φ \to (f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f \leftrightarrow f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f)$
28	21 24 27	3imtr3d	$⊢ φ \to ((x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y)) \to f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f)$
29	28	3expd	$⊢ φ \to (x \in {Base}_{C} \to (y \in {Base}_{C} \to (f \in (x Hom (C) y) \to f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f)))$
30	29	imp41	$⊢ (((φ \land x \in {Base}_{C}) \land y \in {Base}_{C}) \land f \in (x Hom (C) y)) \to f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f$
31	30	ralrimiva	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{C}) \to \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f$
32	20 31	jca	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{C}) \to (\forall f \in (y Hom (C) x) \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f)$
33	32	ralrimiva	$⊢ (φ \land x \in {Base}_{C}) \to \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f)$
34	5	ex	$⊢ φ \to (x \in B \to \underset{˙}{1} \in (x H x))$
35	2	oveqd	$⊢ φ \to x H x = x Hom (C) x$
36	35	eleq2d	$⊢ φ \to (\underset{˙}{1} \in (x H x) \leftrightarrow \underset{˙}{1} \in (x Hom (C) x))$
37	34 9 36	3imtr3d	$⊢ φ \to (x \in {Base}_{C} \to \underset{˙}{1} \in (x Hom (C) x))$
38	37	imp	$⊢ (φ \land x \in {Base}_{C}) \to \underset{˙}{1} \in (x Hom (C) x)$
39		eqid	$⊢ {Base}_{C} = {Base}_{C}$
40		eqid	$⊢ Hom (C) = Hom (C)$
41		eqid	$⊢ comp (C) = comp (C)$
42	4	adantr	$⊢ (φ \land x \in {Base}_{C}) \to C \in Cat$
43		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
44	39 40 41 42 43	catideu	$⊢ (φ \land x \in {Base}_{C}) \to \exists! g \in (x Hom (C) x) \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)$
45		oveq1	$⊢ g = \underset{˙}{1} \to g (⟨y, x⟩ comp (C) x) f = \underset{˙}{1} (⟨y, x⟩ comp (C) x) f$
46	45	eqeq1d	$⊢ g = \underset{˙}{1} \to (g (⟨y, x⟩ comp (C) x) f = f \leftrightarrow \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f)$
47	46	ralbidv	$⊢ g = \underset{˙}{1} \to (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \leftrightarrow \forall f \in (y Hom (C) x) \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f)$
48		oveq2	$⊢ g = \underset{˙}{1} \to f (⟨x, x⟩ comp (C) y) g = f (⟨x, x⟩ comp (C) y) \underset{˙}{1}$
49	48	eqeq1d	$⊢ g = \underset{˙}{1} \to (f (⟨x, x⟩ comp (C) y) g = f \leftrightarrow f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f)$
50	49	ralbidv	$⊢ g = \underset{˙}{1} \to (\forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f \leftrightarrow \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f)$
51	47 50	anbi12d	$⊢ g = \underset{˙}{1} \to ((\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f) \leftrightarrow (\forall f \in (y Hom (C) x) \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f))$
52	51	ralbidv	$⊢ g = \underset{˙}{1} \to (\forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f) \leftrightarrow \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f))$
53	52	riota2	$⊢ (\underset{˙}{1} \in (x Hom (C) x) \land \exists! g \in (x Hom (C) x) \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)) \to (\forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f) \leftrightarrow (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)) = \underset{˙}{1})$
54	38 44 53	syl2anc	$⊢ (φ \land x \in {Base}_{C}) \to (\forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) \underset{˙}{1} (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) \underset{˙}{1} = f) \leftrightarrow (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)) = \underset{˙}{1})$
55	33 54	mpbid	$⊢ (φ \land x \in {Base}_{C}) \to (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)) = \underset{˙}{1}$
56	55	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f))) = (x \in {Base}_{C} ⟼ \underset{˙}{1})$
57		eqid	$⊢ Id (C) = Id (C)$
58	39 40 41 4 57	cidfval	$⊢ φ \to Id (C) = (x \in {Base}_{C} ⟼ (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)))$
59	1	mpteq1d	$⊢ φ \to (x \in B ⟼ \underset{˙}{1}) = (x \in {Base}_{C} ⟼ \underset{˙}{1})$
60	56 58 59	3eqtr4d	$⊢ φ \to Id (C) = (x \in B ⟼ \underset{˙}{1})$

Metamath Proof Explorer

Theorem catidd

Proof