yonedalem21

	Ref	Expression
Hypotheses	yoneda.y	$⊢ Y = Yon (C)$
	yoneda.b	$⊢ B = {Base}_{C}$
	yoneda.1	$⊢ \underset{˙}{1} = Id (C)$
	yoneda.o	$⊢ O = oppCat (C)$
	yoneda.s	$⊢ S = SetCat (U)$
	yoneda.t	$⊢ T = SetCat (V)$
	yoneda.q	$⊢ Q = O FuncCat S$
	yoneda.h	$⊢ H = {Hom}_{F} (Q)$
	yoneda.r	$⊢ R = (Q \times_{c} O) FuncCat T$
	yoneda.e	$⊢ E = O {eval}_{F} S$
	yoneda.z	$⊢ Z = H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))$
	yoneda.c	$⊢ φ \to C \in Cat$
	yoneda.w	$⊢ φ \to V \in W$
	yoneda.u	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
	yoneda.v	$⊢ φ \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
	yonedalem21.f	$⊢ φ \to F \in (O Func S)$
	yonedalem21.x	$⊢ φ \to X \in B$
Assertion	yonedalem21	$⊢ φ \to F 1^{st} (Z) X = 1^{st} (Y) (X) (O Nat S) F$

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	$⊢ Y = Yon (C)$
2		yoneda.b	$⊢ B = {Base}_{C}$
3		yoneda.1	$⊢ \underset{˙}{1} = Id (C)$
4		yoneda.o	$⊢ O = oppCat (C)$
5		yoneda.s	$⊢ S = SetCat (U)$
6		yoneda.t	$⊢ T = SetCat (V)$
7		yoneda.q	$⊢ Q = O FuncCat S$
8		yoneda.h	$⊢ H = {Hom}_{F} (Q)$
9		yoneda.r	$⊢ R = (Q \times_{c} O) FuncCat T$
10		yoneda.e	$⊢ E = O {eval}_{F} S$
11		yoneda.z	$⊢ Z = H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))$
12		yoneda.c	$⊢ φ \to C \in Cat$
13		yoneda.w	$⊢ φ \to V \in W$
14		yoneda.u	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
15		yoneda.v	$⊢ φ \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
16		yonedalem21.f	$⊢ φ \to F \in (O Func S)$
17		yonedalem21.x	$⊢ φ \to X \in B$
18	11	fveq2i	$⊢ 1^{st} (Z) = 1^{st} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)))$
19	18	oveqi	$⊢ F 1^{st} (Z) X = F 1^{st} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) X$
20		df-ov	$⊢ F 1^{st} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) X = 1^{st} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) (⟨F, X⟩)$
21	19 20	eqtri	$⊢ F 1^{st} (Z) X = 1^{st} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) (⟨F, X⟩)$
22		eqid	$⊢ Q \times_{c} O = Q \times_{c} O$
23	7	fucbas	$⊢ O Func S = {Base}_{Q}$
24	4 2	oppcbas	$⊢ B = {Base}_{O}$
25	22 23 24	xpcbas	$⊢ (O Func S) \times B = {Base}_{(Q \times_{c} O)}$
26		eqid	$⊢ (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O) = (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)$
27		eqid	$⊢ oppCat (Q) \times_{c} Q = oppCat (Q) \times_{c} Q$
28	4	oppccat	$⊢ C \in Cat \to O \in Cat$
29	12 28	syl	$⊢ φ \to O \in Cat$
30	15	unssbd	$⊢ φ \to U \subseteq V$
31	13 30	ssexd	$⊢ φ \to U \in V$
32	5	setccat	$⊢ U \in V \to S \in Cat$
33	31 32	syl	$⊢ φ \to S \in Cat$
34	7 29 33	fuccat	$⊢ φ \to Q \in Cat$
35		eqid	$⊢ Q {2^{nd}}_{F} O = Q {2^{nd}}_{F} O$
36	22 34 29 35	2ndfcl	$⊢ φ \to Q {2^{nd}}_{F} O \in ((Q \times_{c} O) Func O)$
37		eqid	$⊢ oppCat (Q) = oppCat (Q)$
38		relfunc	$⊢ Rel (C Func Q)$
39	1 12 4 5 7 31 14	yoncl	$⊢ φ \to Y \in (C Func Q)$
40		1st2ndbr	$⊢ (Rel (C Func Q) \land Y \in (C Func Q)) \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
41	38 39 40	sylancr	$⊢ φ \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
42	4 37 41	funcoppc	$⊢ φ \to 1^{st} (Y) (O Func oppCat (Q)) tpos 2^{nd} (Y)$
43		df-br	$⊢ 1^{st} (Y) (O Func oppCat (Q)) tpos 2^{nd} (Y) \leftrightarrow ⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \in (O Func oppCat (Q))$
44	42 43	sylib	$⊢ φ \to ⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \in (O Func oppCat (Q))$
45	36 44	cofucl	$⊢ φ \to ⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O) \in ((Q \times_{c} O) Func oppCat (Q))$
46		eqid	$⊢ Q {1^{st}}_{F} O = Q {1^{st}}_{F} O$
47	22 34 29 46	1stfcl	$⊢ φ \to Q {1^{st}}_{F} O \in ((Q \times_{c} O) Func Q)$
48	26 27 45 47	prfcl	$⊢ φ \to (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O) \in ((Q \times_{c} O) Func (oppCat (Q) \times_{c} Q))$
49	15	unssad	$⊢ φ \to ran {Hom}_{𝑓} (Q) \subseteq V$
50	8 37 6 34 13 49	hofcl	$⊢ φ \to H \in ((oppCat (Q) \times_{c} Q) Func T)$
51	16 17	opelxpd	$⊢ φ \to ⟨F, X⟩ \in ((O Func S) \times B)$
52	25 48 50 51	cofu1	$⊢ φ \to 1^{st} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) (⟨F, X⟩) = 1^{st} (H) (1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨F, X⟩))$
53	21 52	eqtrid	$⊢ φ \to F 1^{st} (Z) X = 1^{st} (H) (1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨F, X⟩))$
54		eqid	$⊢ Hom (Q \times_{c} O) = Hom (Q \times_{c} O)$
55	26 25 54 45 47 51	prf1	$⊢ φ \to 1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨F, X⟩) = ⟨1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) (⟨F, X⟩), 1^{st} (Q {1^{st}}_{F} O) (⟨F, X⟩)⟩$
56	25 36 44 51	cofu1	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) (⟨F, X⟩) = 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) (1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩))$
57		fvex	$⊢ 1^{st} (Y) \in V$
58		fvex	$⊢ 2^{nd} (Y) \in V$
59	58	tposex	$⊢ tpos 2^{nd} (Y) \in V$
60	57 59	op1st	$⊢ 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) = 1^{st} (Y)$
61	60	a1i	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) = 1^{st} (Y)$
62	22 25 54 34 29 35 51	2ndf1	$⊢ φ \to 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) = 2^{nd} (⟨F, X⟩)$
63		op2ndg	$⊢ (F \in (O Func S) \land X \in B) \to 2^{nd} (⟨F, X⟩) = X$
64	16 17 63	syl2anc	$⊢ φ \to 2^{nd} (⟨F, X⟩) = X$
65	62 64	eqtrd	$⊢ φ \to 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) = X$
66	61 65	fveq12d	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) (1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩)) = 1^{st} (Y) (X)$
67	56 66	eqtrd	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) (⟨F, X⟩) = 1^{st} (Y) (X)$
68	22 25 54 34 29 46 51	1stf1	$⊢ φ \to 1^{st} (Q {1^{st}}_{F} O) (⟨F, X⟩) = 1^{st} (⟨F, X⟩)$
69		op1stg	$⊢ (F \in (O Func S) \land X \in B) \to 1^{st} (⟨F, X⟩) = F$
70	16 17 69	syl2anc	$⊢ φ \to 1^{st} (⟨F, X⟩) = F$
71	68 70	eqtrd	$⊢ φ \to 1^{st} (Q {1^{st}}_{F} O) (⟨F, X⟩) = F$
72	67 71	opeq12d	$⊢ φ \to ⟨1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) (⟨F, X⟩), 1^{st} (Q {1^{st}}_{F} O) (⟨F, X⟩)⟩ = ⟨1^{st} (Y) (X), F⟩$
73	55 72	eqtrd	$⊢ φ \to 1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨F, X⟩) = ⟨1^{st} (Y) (X), F⟩$
74	73	fveq2d	$⊢ φ \to 1^{st} (H) (1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨F, X⟩)) = 1^{st} (H) (⟨1^{st} (Y) (X), F⟩)$
75		df-ov	$⊢ 1^{st} (Y) (X) 1^{st} (H) F = 1^{st} (H) (⟨1^{st} (Y) (X), F⟩)$
76	74 75	eqtr4di	$⊢ φ \to 1^{st} (H) (1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨F, X⟩)) = 1^{st} (Y) (X) 1^{st} (H) F$
77		eqid	$⊢ O Nat S = O Nat S$
78	7 77	fuchom	$⊢ O Nat S = Hom (Q)$
79	1 2 12 17 4 5 31 14	yon1cl	$⊢ φ \to 1^{st} (Y) (X) \in (O Func S)$
80	8 34 23 78 79 16	hof1	$⊢ φ \to 1^{st} (Y) (X) 1^{st} (H) F = 1^{st} (Y) (X) (O Nat S) F$
81	53 76 80	3eqtrd	$⊢ φ \to F 1^{st} (Z) X = 1^{st} (Y) (X) (O Nat S) F$

Metamath Proof Explorer

Theorem yonedalem21

Proof