catrid

Description: Right 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	catrid	$⊢ φ \to F (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X) = 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		oveq1	$⊢ f = F \to f (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X) = F (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X)$
10		id	$⊢ f = F \to f = F$
11	9 10	eqeq12d	$⊢ f = F \to (f (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X) = f \leftrightarrow F (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X) = F)$
12		oveq2	$⊢ y = Y \to X H y = X H Y$
13		oveq2	$⊢ y = Y \to ⟨X, X⟩ \underset{˙}{\cdot} y = ⟨X, X⟩ \underset{˙}{\cdot} Y$
14	13	oveqd	$⊢ y = Y \to f (⟨X, X⟩ \underset{˙}{\cdot} y) \underset{˙}{1} (X) = f (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X)$
15	14	eqeq1d	$⊢ y = Y \to (f (⟨X, X⟩ \underset{˙}{\cdot} y) \underset{˙}{1} (X) = f \leftrightarrow f (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X) = f)$
16	12 15	raleqbidv	$⊢ y = Y \to (\forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) \underset{˙}{1} (X) = f \leftrightarrow \forall f \in (X H Y) f (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X) = f)$
17		simpr	$⊢ (\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) \to \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f$
18	17	ralimi	$⊢ \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) \to \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f$
19	18	a1i	$⊢ g \in (X H 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) \to \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f)$
20	19	ss2rabi	$⊢ \{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)\} \subseteq \{g \in (X H X) \| \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f\}$
21	1 2 6 4 3 5	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))$
22	1 2 6 4 5	catideu	$⊢ φ \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)$
23		riotacl2	$⊢ \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) \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 \{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)\}$
24	22 23	syl	$⊢ φ \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 \{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	21 24	eqeltrd	$⊢ φ \to \underset{˙}{1} (X) \in \{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	20 25	sselid	$⊢ φ \to \underset{˙}{1} (X) \in \{g \in (X H X) \| \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f\}$
27		oveq2	$⊢ g = \underset{˙}{1} (X) \to f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f (⟨X, X⟩ \underset{˙}{\cdot} y) \underset{˙}{1} (X)$
28	27	eqeq1d	$⊢ g = \underset{˙}{1} (X) \to (f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow f (⟨X, X⟩ \underset{˙}{\cdot} y) \underset{˙}{1} (X) = f)$
29	28	2ralbidv	$⊢ g = \underset{˙}{1} (X) \to (\forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) \underset{˙}{1} (X) = f)$
30	29	elrab	$⊢ \underset{˙}{1} (X) \in \{g \in (X H X) \| \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f\} \leftrightarrow (\underset{˙}{1} (X) \in (X H X) \land \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) \underset{˙}{1} (X) = f)$
31	30	simprbi	$⊢ \underset{˙}{1} (X) \in \{g \in (X H X) \| \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) g = f\} \to \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) \underset{˙}{1} (X) = f$
32	26 31	syl	$⊢ φ \to \forall y \in B \forall f \in (X H y) f (⟨X, X⟩ \underset{˙}{\cdot} y) \underset{˙}{1} (X) = f$
33	16 32 7	rspcdva	$⊢ φ \to \forall f \in (X H Y) f (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X) = f$
34	11 33 8	rspcdva	$⊢ φ \to F (⟨X, X⟩ \underset{˙}{\cdot} Y) \underset{˙}{1} (X) = F$

Metamath Proof Explorer

Theorem catrid

Proof