yonedalem1

	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$
Assertion	yonedalem1	$⊢ φ \to (Z \in ((Q \times_{c} O) Func T) \land E \in ((Q \times_{c} O) Func T))$

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		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)$
17		eqid	$⊢ oppCat (Q) \times_{c} Q = oppCat (Q) \times_{c} Q$
18		eqid	$⊢ Q \times_{c} O = Q \times_{c} O$
19	4	oppccat	$⊢ C \in Cat \to O \in Cat$
20	12 19	syl	$⊢ φ \to O \in Cat$
21	15	unssbd	$⊢ φ \to U \subseteq V$
22	13 21	ssexd	$⊢ φ \to U \in V$
23	5	setccat	$⊢ U \in V \to S \in Cat$
24	22 23	syl	$⊢ φ \to S \in Cat$
25	7 20 24	fuccat	$⊢ φ \to Q \in Cat$
26		eqid	$⊢ Q {2^{nd}}_{F} O = Q {2^{nd}}_{F} O$
27	18 25 20 26	2ndfcl	$⊢ φ \to Q {2^{nd}}_{F} O \in ((Q \times_{c} O) Func O)$
28		eqid	$⊢ oppCat (Q) = oppCat (Q)$
29		relfunc	$⊢ Rel (C Func Q)$
30	1 12 4 5 7 22 14	yoncl	$⊢ φ \to Y \in (C Func Q)$
31		1st2ndbr	$⊢ (Rel (C Func Q) \land Y \in (C Func Q)) \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
32	29 30 31	sylancr	$⊢ φ \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
33	4 28 32	funcoppc	$⊢ φ \to 1^{st} (Y) (O Func oppCat (Q)) tpos 2^{nd} (Y)$
34		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))$
35	33 34	sylib	$⊢ φ \to ⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \in (O Func oppCat (Q))$
36	27 35	cofucl	$⊢ φ \to ⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O) \in ((Q \times_{c} O) Func oppCat (Q))$
37		eqid	$⊢ Q {1^{st}}_{F} O = Q {1^{st}}_{F} O$
38	18 25 20 37	1stfcl	$⊢ φ \to Q {1^{st}}_{F} O \in ((Q \times_{c} O) Func Q)$
39	16 17 36 38	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))$
40	15	unssad	$⊢ φ \to ran {Hom}_{𝑓} (Q) \subseteq V$
41	8 28 6 25 13 40	hofcl	$⊢ φ \to H \in ((oppCat (Q) \times_{c} Q) Func T)$
42	39 41	cofucl	$⊢ φ \to H \circ_{func} ((⟨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 T)$
43	11 42	eqeltrid	$⊢ φ \to Z \in ((Q \times_{c} O) Func T)$
44	6 5 13 21	funcsetcres2	$⊢ φ \to (Q \times_{c} O) Func S \subseteq (Q \times_{c} O) Func T$
45	10 7 20 24	evlfcl	$⊢ φ \to E \in ((Q \times_{c} O) Func S)$
46	44 45	sseldd	$⊢ φ \to E \in ((Q \times_{c} O) Func T)$
47	43 46	jca	$⊢ φ \to (Z \in ((Q \times_{c} O) Func T) \land E \in ((Q \times_{c} O) Func T))$

Metamath Proof Explorer

Theorem yonedalem1

Proof