idfu2nd

Description: Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Step	Hyp	Ref	Expression
1		idfuval.i	$⊢ I = {id}_{func} (C)$
2		idfuval.b	$⊢ B = {Base}_{C}$
3		idfuval.c	$⊢ φ \to C \in Cat$
4		idfuval.h	$⊢ H = Hom (C)$
5		idfu2nd.x	$⊢ φ \to X \in B$
6		idfu2nd.y	$⊢ φ \to Y \in B$
7		df-ov	$⊢ X 2^{nd} (I) Y = 2^{nd} (I) (⟨X, Y⟩)$
8	1 2 3 4	idfuval	$⊢ φ \to I = ⟨{I ↾}_{B}, (z \in (B \times B) ⟼ {I ↾}_{H (z)})⟩$
9	8	fveq2d	$⊢ φ \to 2^{nd} (I) = 2^{nd} (⟨{I ↾}_{B}, (z \in (B \times B) ⟼ {I ↾}_{H (z)})⟩)$
10	2	fvexi	$⊢ B \in V$
11		resiexg	$⊢ B \in V \to {I ↾}_{B} \in V$
12	10 11	ax-mp	$⊢ {I ↾}_{B} \in V$
13	10 10	xpex	$⊢ B \times B \in V$
14	13	mptex	$⊢ (z \in (B \times B) ⟼ {I ↾}_{H (z)}) \in V$
15	12 14	op2nd	$⊢ 2^{nd} (⟨{I ↾}_{B}, (z \in (B \times B) ⟼ {I ↾}_{H (z)})⟩) = (z \in (B \times B) ⟼ {I ↾}_{H (z)})$
16	9 15	eqtrdi	$⊢ φ \to 2^{nd} (I) = (z \in (B \times B) ⟼ {I ↾}_{H (z)})$
17		simpr	$⊢ (φ \land z = ⟨X, Y⟩) \to z = ⟨X, Y⟩$
18	17	fveq2d	$⊢ (φ \land z = ⟨X, Y⟩) \to H (z) = H (⟨X, Y⟩)$
19		df-ov	$⊢ X H Y = H (⟨X, Y⟩)$
20	18 19	eqtr4di	$⊢ (φ \land z = ⟨X, Y⟩) \to H (z) = X H Y$
21	20	reseq2d	$⊢ (φ \land z = ⟨X, Y⟩) \to {I ↾}_{H (z)} = {I ↾}_{(X H Y)}$
22	5 6	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
23		ovex	$⊢ X H Y \in V$
24		resiexg	$⊢ X H Y \in V \to {I ↾}_{(X H Y)} \in V$
25	23 24	mp1i	$⊢ φ \to {I ↾}_{(X H Y)} \in V$
26	16 21 22 25	fvmptd	$⊢ φ \to 2^{nd} (I) (⟨X, Y⟩) = {I ↾}_{(X H Y)}$
27	7 26	syl5eq	$⊢ φ \to X 2^{nd} (I) Y = {I ↾}_{(X H Y)}$

Metamath Proof Explorer