catlid

Description: Left identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	catidcl.b	$⊢ B = {Base}_{C}$
	catidcl.h	$⊢ H = Hom (C)$
	catidcl.i	$⊢ \underset{˙}{1} = Id (C)$
	catidcl.c	$⊢ φ \to C \in Cat$
	catidcl.x	$⊢ φ \to X \in B$
	catlid.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	catlid.y	$⊢ φ \to Y \in B$
	catlid.f	$⊢ φ \to F \in (X H Y)$
Assertion	catlid	$⊢ φ \to \underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) F = F$

Proof

Step	Hyp	Ref	Expression
1		catidcl.b	$⊢ B = {Base}_{C}$
2		catidcl.h	$⊢ H = Hom (C)$
3		catidcl.i	$⊢ \underset{˙}{1} = Id (C)$
4		catidcl.c	$⊢ φ \to C \in Cat$
5		catidcl.x	$⊢ φ \to X \in B$
6		catlid.o	$⊢ \underset{˙}{\cdot} = comp (C)$
7		catlid.y	$⊢ φ \to Y \in B$
8		catlid.f	$⊢ φ \to F \in (X H Y)$
9		oveq2	$⊢ f = F \to \underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) f = \underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) F$
10		id	$⊢ f = F \to f = F$
11	9 10	eqeq12d	$⊢ f = F \to (\underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) f = f \leftrightarrow \underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) F = F)$
12		oveq1	$⊢ x = X \to x H Y = X H Y$
13		opeq1	$⊢ x = X \to ⟨x, Y⟩ = ⟨X, Y⟩$
14	13	oveq1d	$⊢ x = X \to ⟨x, Y⟩ \underset{˙}{\cdot} Y = ⟨X, Y⟩ \underset{˙}{\cdot} Y$
15	14	oveqd	$⊢ x = X \to \underset{˙}{1} (Y) (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = \underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) f$
16	15	eqeq1d	$⊢ x = X \to (\underset{˙}{1} (Y) (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \leftrightarrow \underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) f = f)$
17	12 16	raleqbidv	$⊢ x = X \to (\forall f \in (x H Y) \underset{˙}{1} (Y) (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \leftrightarrow \forall f \in (X H Y) \underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) f = f)$
18		simpl	$⊢ (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f) \to \forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f$
19	18	ralimi	$⊢ \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f) \to \forall x \in B \forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f$
20	19	a1i	$⊢ g \in (Y H Y) \to (\forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f) \to \forall x \in B \forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f)$
21	20	ss2rabi	$⊢ \{g \in (Y H Y) \| \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f)\} \subseteq \{g \in (Y H Y) \| \forall x \in B \forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f\}$
22	1 2 6 4 3 7	cidval	$⊢ φ \to \underset{˙}{1} (Y) = (ι g \in (Y H Y) \| \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f))$
23	1 2 6 4 7	catideu	$⊢ φ \to \exists! g \in (Y H Y) \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f)$
24		riotacl2	$⊢ \exists! g \in (Y H Y) \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f) \to (ι g \in (Y H Y) \| \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f)) \in \{g \in (Y H Y) \| \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f)\}$
25	23 24	syl	$⊢ φ \to (ι g \in (Y H Y) \| \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f)) \in \{g \in (Y H Y) \| \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f)\}$
26	22 25	eqeltrd	$⊢ φ \to \underset{˙}{1} (Y) \in \{g \in (Y H Y) \| \forall x \in B (\forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \land \forall f \in (Y H x) f (⟨Y, Y⟩ \underset{˙}{\cdot} x) g = f)\}$
27	21 26	sseldi	$⊢ φ \to \underset{˙}{1} (Y) \in \{g \in (Y H Y) \| \forall x \in B \forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f\}$
28		oveq1	$⊢ g = \underset{˙}{1} (Y) \to g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = \underset{˙}{1} (Y) (⟨x, Y⟩ \underset{˙}{\cdot} Y) f$
29	28	eqeq1d	$⊢ g = \underset{˙}{1} (Y) \to (g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \leftrightarrow \underset{˙}{1} (Y) (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f)$
30	29	2ralbidv	$⊢ g = \underset{˙}{1} (Y) \to (\forall x \in B \forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f \leftrightarrow \forall x \in B \forall f \in (x H Y) \underset{˙}{1} (Y) (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f)$
31	30	elrab	$⊢ \underset{˙}{1} (Y) \in \{g \in (Y H Y) \| \forall x \in B \forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f\} \leftrightarrow (\underset{˙}{1} (Y) \in (Y H Y) \land \forall x \in B \forall f \in (x H Y) \underset{˙}{1} (Y) (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f)$
32	31	simprbi	$⊢ \underset{˙}{1} (Y) \in \{g \in (Y H Y) \| \forall x \in B \forall f \in (x H Y) g (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f\} \to \forall x \in B \forall f \in (x H Y) \underset{˙}{1} (Y) (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f$
33	27 32	syl	$⊢ φ \to \forall x \in B \forall f \in (x H Y) \underset{˙}{1} (Y) (⟨x, Y⟩ \underset{˙}{\cdot} Y) f = f$
34	17 33 5	rspcdva	$⊢ φ \to \forall f \in (X H Y) \underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) f = f$
35	11 34 8	rspcdva	$⊢ φ \to \underset{˙}{1} (Y) (⟨X, Y⟩ \underset{˙}{\cdot} Y) F = F$

Metamath Proof Explorer

Theorem catlid

Proof