cidfval

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

	Ref	Expression
Hypotheses	cidfval.b	$⊢ B = {Base}_{C}$
	cidfval.h	$⊢ H = Hom (C)$
	cidfval.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	cidfval.c	$⊢ φ \to C \in Cat$
	cidfval.i	$⊢ \underset{˙}{1} = Id (C)$
Assertion	cidfval	$⊢ φ \to \underset{˙}{1} = (x \in B ⟼ (ι 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		cidfval.b	$⊢ B = {Base}_{C}$
2		cidfval.h	$⊢ H = Hom (C)$
3		cidfval.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		cidfval.c	$⊢ φ \to C \in Cat$
5		cidfval.i	$⊢ \underset{˙}{1} = Id (C)$
6		fvexd	$⊢ c = C \to {Base}_{c} \in V$
7		fveq2	$⊢ c = C \to {Base}_{c} = {Base}_{C}$
8	7 1	syl6eqr	$⊢ c = C \to {Base}_{c} = B$
9		fvexd	$⊢ (c = C \land b = B) \to Hom (c) \in V$
10		simpl	$⊢ (c = C \land b = B) \to c = C$
11	10	fveq2d	$⊢ (c = C \land b = B) \to Hom (c) = Hom (C)$
12	11 2	syl6eqr	$⊢ (c = C \land b = B) \to Hom (c) = H$
13		fvexd	$⊢ ((c = C \land b = B) \land h = H) \to comp (c) \in V$
14		simpll	$⊢ ((c = C \land b = B) \land h = H) \to c = C$
15	14	fveq2d	$⊢ ((c = C \land b = B) \land h = H) \to comp (c) = comp (C)$
16	15 3	syl6eqr	$⊢ ((c = C \land b = B) \land h = H) \to comp (c) = \underset{˙}{\cdot}$
17		simpllr	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to b = B$
18		simplr	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to h = H$
19	18	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to x h x = x H x$
20	18	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to y h x = y H x$
21		simpr	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to o = \underset{˙}{\cdot}$
22	21	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ⟨y, x⟩ o x = ⟨y, x⟩ \underset{˙}{\cdot} x$
23	22	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to g (⟨y, x⟩ o x) f = g (⟨y, x⟩ \underset{˙}{\cdot} x) f$
24	23	eqeq1d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (g (⟨y, x⟩ o x) f = f \leftrightarrow g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f)$
25	20 24	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \leftrightarrow \forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f)$
26	18	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to x h y = x H y$
27	21	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ⟨x, x⟩ o y = ⟨x, x⟩ \underset{˙}{\cdot} y$
28	27	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to f (⟨x, x⟩ o y) g = f (⟨x, x⟩ \underset{˙}{\cdot} y) g$
29	28	eqeq1d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (f (⟨x, x⟩ o y) g = f \leftrightarrow f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f)$
30	26 29	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall f \in (x h y) f (⟨x, x⟩ o y) g = f \leftrightarrow \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f)$
31	25 30	anbi12d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ((\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o 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))$
32	17 31	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o 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))$
33	19 32	riotaeqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (ι g \in (x h x) \| \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o y) g = f)) = (ι 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))$
34	17 33	mpteq12dv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (x \in b ⟼ (ι g \in (x h x) \| \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o y) g = f))) = (x \in B ⟼ (ι 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)))$
35	13 16 34	csbied2	$⊢ ((c = C \land b = B) \land h = H) \to ⦋ comp (c) / o ⦌ (x \in b ⟼ (ι g \in (x h x) \| \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o y) g = f))) = (x \in B ⟼ (ι 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)))$
36	9 12 35	csbied2	$⊢ (c = C \land b = B) \to ⦋ Hom (c) / h ⦌ ⦋ comp (c) / o ⦌ (x \in b ⟼ (ι g \in (x h x) \| \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o y) g = f))) = (x \in B ⟼ (ι 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)))$
37	6 8 36	csbied2	$⊢ c = C \to ⦋ {Base}_{c} / b ⦌ ⦋ Hom (c) / h ⦌ ⦋ comp (c) / o ⦌ (x \in b ⟼ (ι g \in (x h x) \| \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o y) g = f))) = (x \in B ⟼ (ι 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)))$
38		df-cid	$⊢ Id = (c \in Cat ⟼ ⦋ {Base}_{c} / b ⦌ ⦋ Hom (c) / h ⦌ ⦋ comp (c) / o ⦌ (x \in b ⟼ (ι g \in (x h x) \| \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o y) g = f))))$
39	37 38 1	mptfvmpt	$⊢ C \in Cat \to Id (C) = (x \in B ⟼ (ι 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)))$
40	4 39	syl	$⊢ φ \to Id (C) = (x \in B ⟼ (ι 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)))$
41	5 40	syl5eq	$⊢ φ \to \underset{˙}{1} = (x \in B ⟼ (ι 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 cidfval

Proof