cidval

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-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)$
	cidval.x	$⊢ φ \to X \in B$
Assertion	cidval	$⊢ φ \to \underset{˙}{1} (X) = (ι 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		cidval.x	$⊢ φ \to X \in B$
7	1 2 3 4 5	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)))$
8		simpr	$⊢ (φ \land x = X) \to x = X$
9	8 8	oveq12d	$⊢ (φ \land x = X) \to x H x = X H X$
10	8	oveq2d	$⊢ (φ \land x = X) \to y H x = y H X$
11	8	opeq2d	$⊢ (φ \land x = X) \to ⟨y, x⟩ = ⟨y, X⟩$
12	11 8	oveq12d	$⊢ (φ \land x = X) \to ⟨y, x⟩ \underset{˙}{\cdot} x = ⟨y, X⟩ \underset{˙}{\cdot} X$
13	12	oveqd	$⊢ (φ \land x = X) \to g (⟨y, x⟩ \underset{˙}{\cdot} x) f = g (⟨y, X⟩ \underset{˙}{\cdot} X) f$
14	13	eqeq1d	$⊢ (φ \land x = X) \to (g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \leftrightarrow g (⟨y, X⟩ \underset{˙}{\cdot} X) f = f)$
15	10 14	raleqbidv	$⊢ (φ \land 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)$
16	8	oveq1d	$⊢ (φ \land x = X) \to x H y = X H y$
17	8 8	opeq12d	$⊢ (φ \land x = X) \to ⟨x, x⟩ = ⟨X, X⟩$
18	17	oveq1d	$⊢ (φ \land x = X) \to ⟨x, x⟩ \underset{˙}{\cdot} y = ⟨X, X⟩ \underset{˙}{\cdot} y$
19	18	oveqd	$⊢ (φ \land x = X) \to f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f (⟨X, X⟩ \underset{˙}{\cdot} y) g$
20	19	eqeq1d	$⊢ (φ \land x = X) \to (f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f)$
21	16 20	raleqbidv	$⊢ (φ \land 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)$
22	15 21	anbi12d	$⊢ (φ \land 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))$
23	22	ralbidv	$⊢ (φ \land 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))$
24	9 23	riotaeqbidv	$⊢ (φ \land x = X) \to (ι 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)) = (ι 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))$
25		riotaex	$⊢ (ι 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)) \in V$
26	25	a1i	$⊢ φ \to (ι 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)) \in V$
27	7 24 6 26	fvmptd	$⊢ φ \to \underset{˙}{1} (X) = (ι 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 cidval

Proof