yon2

Description: Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017)

	Ref	Expression
Hypotheses	yon11.y	$⊢ Y = Yon (C)$
	yon11.b	$⊢ B = {Base}_{C}$
	yon11.c	$⊢ φ \to C \in Cat$
	yon11.p	$⊢ φ \to X \in B$
	yon11.h	$⊢ H = Hom (C)$
	yon11.z	$⊢ φ \to Z \in B$
	yon12.x	$⊢ \underset{˙}{\cdot} = comp (C)$
	yon12.w	$⊢ φ \to W \in B$
	yon2.f	$⊢ φ \to F \in (X H Z)$
	yon2.g	$⊢ φ \to G \in (W H X)$
Assertion	yon2	$⊢ φ \to (X 2^{nd} (Y) Z) (F) (W) (G) = F (⟨W, X⟩ \underset{˙}{\cdot} Z) G$

Proof

Step	Hyp	Ref	Expression
1		yon11.y	$⊢ Y = Yon (C)$
2		yon11.b	$⊢ B = {Base}_{C}$
3		yon11.c	$⊢ φ \to C \in Cat$
4		yon11.p	$⊢ φ \to X \in B$
5		yon11.h	$⊢ H = Hom (C)$
6		yon11.z	$⊢ φ \to Z \in B$
7		yon12.x	$⊢ \underset{˙}{\cdot} = comp (C)$
8		yon12.w	$⊢ φ \to W \in B$
9		yon2.f	$⊢ φ \to F \in (X H Z)$
10		yon2.g	$⊢ φ \to G \in (W H X)$
11		eqid	$⊢ oppCat (C) = oppCat (C)$
12		eqid	$⊢ {Hom}_{F} (oppCat (C)) = {Hom}_{F} (oppCat (C))$
13	1 3 11 12	yonval	$⊢ φ \to Y = ⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))$
14	13	fveq2d	$⊢ φ \to 2^{nd} (Y) = 2^{nd} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C)))$
15	14	oveqd	$⊢ φ \to X 2^{nd} (Y) Z = X 2^{nd} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) Z$
16	15	fveq1d	$⊢ φ \to (X 2^{nd} (Y) Z) (F) = (X 2^{nd} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) Z) (F)$
17	16	fveq1d	$⊢ φ \to (X 2^{nd} (Y) Z) (F) (W) = (X 2^{nd} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) Z) (F) (W)$
18		eqid	$⊢ ⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C)) = ⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))$
19	11	oppccat	$⊢ C \in Cat \to oppCat (C) \in Cat$
20	3 19	syl	$⊢ φ \to oppCat (C) \in Cat$
21		eqid	$⊢ SetCat (ran {Hom}_{𝑓} (C)) = SetCat (ran {Hom}_{𝑓} (C))$
22		fvex	$⊢ {Hom}_{𝑓} (C) \in V$
23	22	rnex	$⊢ ran {Hom}_{𝑓} (C) \in V$
24	23	a1i	$⊢ φ \to ran {Hom}_{𝑓} (C) \in V$
25		ssidd	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq ran {Hom}_{𝑓} (C)$
26	11 12 21 3 24 25	oppchofcl	$⊢ φ \to {Hom}_{F} (oppCat (C)) \in ((C \times_{c} oppCat (C)) Func SetCat (ran {Hom}_{𝑓} (C)))$
27	11 2	oppcbas	$⊢ B = {Base}_{oppCat (C)}$
28		eqid	$⊢ Id (oppCat (C)) = Id (oppCat (C))$
29		eqid	$⊢ (X 2^{nd} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) Z) (F) = (X 2^{nd} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) Z) (F)$
30	18 2 3 20 26 27 5 28 4 6 9 29 8	curf2val	$⊢ φ \to (X 2^{nd} (⟨C, oppCat (C)⟩ {curry}_{F} {Hom}_{F} (oppCat (C))) Z) (F) (W) = F (⟨X, W⟩ 2^{nd} ({Hom}_{F} (oppCat (C))) ⟨Z, W⟩) Id (oppCat (C)) (W)$
31	17 30	eqtrd	$⊢ φ \to (X 2^{nd} (Y) Z) (F) (W) = F (⟨X, W⟩ 2^{nd} ({Hom}_{F} (oppCat (C))) ⟨Z, W⟩) Id (oppCat (C)) (W)$
32	31	fveq1d	$⊢ φ \to (X 2^{nd} (Y) Z) (F) (W) (G) = (F (⟨X, W⟩ 2^{nd} ({Hom}_{F} (oppCat (C))) ⟨Z, W⟩) Id (oppCat (C)) (W)) (G)$
33		eqid	$⊢ Hom (oppCat (C)) = Hom (oppCat (C))$
34		eqid	$⊢ comp (oppCat (C)) = comp (oppCat (C))$
35	5 11	oppchom	$⊢ Z Hom (oppCat (C)) X = X H Z$
36	9 35	eleqtrrdi	$⊢ φ \to F \in (Z Hom (oppCat (C)) X)$
37	27 33 28 20 8	catidcl	$⊢ φ \to Id (oppCat (C)) (W) \in (W Hom (oppCat (C)) W)$
38	5 11	oppchom	$⊢ X Hom (oppCat (C)) W = W H X$
39	10 38	eleqtrrdi	$⊢ φ \to G \in (X Hom (oppCat (C)) W)$
40	12 20 27 33 4 8 6 8 34 36 37 39	hof2	$⊢ φ \to (F (⟨X, W⟩ 2^{nd} ({Hom}_{F} (oppCat (C))) ⟨Z, W⟩) Id (oppCat (C)) (W)) (G) = (Id (oppCat (C)) (W) (⟨X, W⟩ comp (oppCat (C)) W) G) (⟨Z, X⟩ comp (oppCat (C)) W) F$
41	27 33 28 20 4 34 8 39	catlid	$⊢ φ \to Id (oppCat (C)) (W) (⟨X, W⟩ comp (oppCat (C)) W) G = G$
42	41	oveq1d	$⊢ φ \to (Id (oppCat (C)) (W) (⟨X, W⟩ comp (oppCat (C)) W) G) (⟨Z, X⟩ comp (oppCat (C)) W) F = G (⟨Z, X⟩ comp (oppCat (C)) W) F$
43	2 7 11 6 4 8	oppcco	$⊢ φ \to G (⟨Z, X⟩ comp (oppCat (C)) W) F = F (⟨W, X⟩ \underset{˙}{\cdot} Z) G$
44	42 43	eqtrd	$⊢ φ \to (Id (oppCat (C)) (W) (⟨X, W⟩ comp (oppCat (C)) W) G) (⟨Z, X⟩ comp (oppCat (C)) W) F = F (⟨W, X⟩ \underset{˙}{\cdot} Z) G$
45	32 40 44	3eqtrd	$⊢ φ \to (X 2^{nd} (Y) Z) (F) (W) (G) = F (⟨W, X⟩ \underset{˙}{\cdot} Z) G$

Metamath Proof Explorer

Theorem yon2

Proof