yonedalem3a

	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$
	yonedalem3a.m	$⊢ M = (f \in (O Func S), x \in B ⟼ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))))$
Assertion	yonedalem3a	$⊢ φ \to (F M X = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ a (X) (\underset{˙}{1} (X))) \land (F M X) : F 1^{st} (Z) X ⟶ F 1^{st} (E) X)$

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		yonedalem3a.m	$⊢ M = (f \in (O Func S), x \in B ⟼ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))))$
19		simpr	$⊢ (f = F \land x = X) \to x = X$
20	19	fveq2d	$⊢ (f = F \land x = X) \to 1^{st} (Y) (x) = 1^{st} (Y) (X)$
21		simpl	$⊢ (f = F \land x = X) \to f = F$
22	20 21	oveq12d	$⊢ (f = F \land x = X) \to 1^{st} (Y) (x) (O Nat S) f = 1^{st} (Y) (X) (O Nat S) F$
23	19	fveq2d	$⊢ (f = F \land x = X) \to a (x) = a (X)$
24	19	fveq2d	$⊢ (f = F \land x = X) \to \underset{˙}{1} (x) = \underset{˙}{1} (X)$
25	23 24	fveq12d	$⊢ (f = F \land x = X) \to a (x) (\underset{˙}{1} (x)) = a (X) (\underset{˙}{1} (X))$
26	22 25	mpteq12dv	$⊢ (f = F \land x = X) \to (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))) = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ a (X) (\underset{˙}{1} (X)))$
27		ovex	$⊢ 1^{st} (Y) (X) (O Nat S) F \in V$
28	27	mptex	$⊢ (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ a (X) (\underset{˙}{1} (X))) \in V$
29	26 18 28	ovmpoa	$⊢ (F \in (O Func S) \land X \in B) \to F M X = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ a (X) (\underset{˙}{1} (X)))$
30	16 17 29	syl2anc	$⊢ φ \to F M X = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ a (X) (\underset{˙}{1} (X)))$
31		eqid	$⊢ O Nat S = O Nat S$
32		simpr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a \in (1^{st} (Y) (X) (O Nat S) F)$
33	31 32	nat1st2nd	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a \in (⟨1^{st} (1^{st} (Y) (X)), 2^{nd} (1^{st} (Y) (X))⟩ (O Nat S) ⟨1^{st} (F), 2^{nd} (F)⟩)$
34	4 2	oppcbas	$⊢ B = {Base}_{O}$
35		eqid	$⊢ Hom (S) = Hom (S)$
36	17	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to X \in B$
37	31 33 34 35 36	natcl	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (X) \in (1^{st} (1^{st} (Y) (X)) (X) Hom (S) 1^{st} (F) (X))$
38	15	unssbd	$⊢ φ \to U \subseteq V$
39	13 38	ssexd	$⊢ φ \to U \in V$
40	39	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to U \in V$
41		eqid	$⊢ {Base}_{S} = {Base}_{S}$
42		relfunc	$⊢ Rel (O Func S)$
43	1 2 12 17 4 5 39 14	yon1cl	$⊢ φ \to 1^{st} (Y) (X) \in (O Func S)$
44		1st2ndbr	$⊢ (Rel (O Func S) \land 1^{st} (Y) (X) \in (O Func S)) \to 1^{st} (1^{st} (Y) (X)) (O Func S) 2^{nd} (1^{st} (Y) (X))$
45	42 43 44	sylancr	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) (O Func S) 2^{nd} (1^{st} (Y) (X))$
46	34 41 45	funcf1	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) : B ⟶ {Base}_{S}$
47	46 17	ffvelcdmd	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) (X) \in {Base}_{S}$
48	5 39	setcbas	$⊢ φ \to U = {Base}_{S}$
49	47 48	eleqtrrd	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) (X) \in U$
50	49	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to 1^{st} (1^{st} (Y) (X)) (X) \in U$
51		1st2ndbr	$⊢ (Rel (O Func S) \land F \in (O Func S)) \to 1^{st} (F) (O Func S) 2^{nd} (F)$
52	42 16 51	sylancr	$⊢ φ \to 1^{st} (F) (O Func S) 2^{nd} (F)$
53	34 41 52	funcf1	$⊢ φ \to 1^{st} (F) : B ⟶ {Base}_{S}$
54	53 17	ffvelcdmd	$⊢ φ \to 1^{st} (F) (X) \in {Base}_{S}$
55	54 48	eleqtrrd	$⊢ φ \to 1^{st} (F) (X) \in U$
56	55	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to 1^{st} (F) (X) \in U$
57	5 40 35 50 56	elsetchom	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (a (X) \in (1^{st} (1^{st} (Y) (X)) (X) Hom (S) 1^{st} (F) (X)) \leftrightarrow a (X) : 1^{st} (1^{st} (Y) (X)) (X) ⟶ 1^{st} (F) (X))$
58	37 57	mpbid	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (X) : 1^{st} (1^{st} (Y) (X)) (X) ⟶ 1^{st} (F) (X)$
59		eqid	$⊢ Hom (C) = Hom (C)$
60	2 59 3 12 17	catidcl	$⊢ φ \to \underset{˙}{1} (X) \in (X Hom (C) X)$
61	1 2 12 17 59 17	yon11	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) (X) = X Hom (C) X$
62	60 61	eleqtrrd	$⊢ φ \to \underset{˙}{1} (X) \in 1^{st} (1^{st} (Y) (X)) (X)$
63	62	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to \underset{˙}{1} (X) \in 1^{st} (1^{st} (Y) (X)) (X)$
64	58 63	ffvelcdmd	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (X) (\underset{˙}{1} (X)) \in 1^{st} (F) (X)$
65	64	fmpttd	$⊢ φ \to (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ a (X) (\underset{˙}{1} (X))) : 1^{st} (Y) (X) (O Nat S) F ⟶ 1^{st} (F) (X)$
66	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	yonedalem21	$⊢ φ \to F 1^{st} (Z) X = 1^{st} (Y) (X) (O Nat S) F$
67	4	oppccat	$⊢ C \in Cat \to O \in Cat$
68	12 67	syl	$⊢ φ \to O \in Cat$
69	5	setccat	$⊢ U \in V \to S \in Cat$
70	39 69	syl	$⊢ φ \to S \in Cat$
71	10 68 70 34 16 17	evlf1	$⊢ φ \to F 1^{st} (E) X = 1^{st} (F) (X)$
72	30 66 71	feq123d	$⊢ φ \to ((F M X) : F 1^{st} (Z) X ⟶ F 1^{st} (E) X \leftrightarrow (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ a (X) (\underset{˙}{1} (X))) : 1^{st} (Y) (X) (O Nat S) F ⟶ 1^{st} (F) (X))$
73	65 72	mpbird	$⊢ φ \to (F M X) : F 1^{st} (Z) X ⟶ F 1^{st} (E) X$
74	30 73	jca	$⊢ φ \to (F M X = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ a (X) (\underset{˙}{1} (X))) \land (F M X) : F 1^{st} (Z) X ⟶ F 1^{st} (E) X)$

Metamath Proof Explorer

Theorem yonedalem3a

Proof