yonedalem4a

	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$
	yonedalem4.n	$⊢ N = (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))))$
	yonedalem4.p	$⊢ φ \to A \in 1^{st} (F) (X)$
Assertion	yonedalem4a	$⊢ φ \to (F N X) (A) = (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (A)))$

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		yonedalem4.n	$⊢ N = (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))))$
19		yonedalem4.p	$⊢ φ \to A \in 1^{st} (F) (X)$
20	18	a1i	$⊢ φ \to N = (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))))$
21		simprl	$⊢ (φ \land (f = F \land x = X)) \to f = F$
22	21	fveq2d	$⊢ (φ \land (f = F \land x = X)) \to 1^{st} (f) = 1^{st} (F)$
23		simprr	$⊢ (φ \land (f = F \land x = X)) \to x = X$
24	22 23	fveq12d	$⊢ (φ \land (f = F \land x = X)) \to 1^{st} (f) (x) = 1^{st} (F) (X)$
25		simplrr	$⊢ ((φ \land (f = F \land x = X)) \land y \in B) \to x = X$
26	25	oveq2d	$⊢ ((φ \land (f = F \land x = X)) \land y \in B) \to y Hom (C) x = y Hom (C) X$
27		simplrl	$⊢ ((φ \land (f = F \land x = X)) \land y \in B) \to f = F$
28	27	fveq2d	$⊢ ((φ \land (f = F \land x = X)) \land y \in B) \to 2^{nd} (f) = 2^{nd} (F)$
29		eqidd	$⊢ ((φ \land (f = F \land x = X)) \land y \in B) \to y = y$
30	28 25 29	oveq123d	$⊢ ((φ \land (f = F \land x = X)) \land y \in B) \to x 2^{nd} (f) y = X 2^{nd} (F) y$
31	30	fveq1d	$⊢ ((φ \land (f = F \land x = X)) \land y \in B) \to (x 2^{nd} (f) y) (g) = (X 2^{nd} (F) y) (g)$
32	31	fveq1d	$⊢ ((φ \land (f = F \land x = X)) \land y \in B) \to (x 2^{nd} (f) y) (g) (u) = (X 2^{nd} (F) y) (g) (u)$
33	26 32	mpteq12dv	$⊢ ((φ \land (f = F \land x = X)) \land y \in B) \to (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)) = (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (u))$
34	33	mpteq2dva	$⊢ (φ \land (f = F \land x = X)) \to (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u))) = (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (u)))$
35	24 34	mpteq12dv	$⊢ (φ \land (f = F \land x = X)) \to (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))) = (u \in 1^{st} (F) (X) ⟼ (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (u))))$
36		fvex	$⊢ 1^{st} (F) (X) \in V$
37	36	mptex	$⊢ (u \in 1^{st} (F) (X) ⟼ (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (u)))) \in V$
38	37	a1i	$⊢ φ \to (u \in 1^{st} (F) (X) ⟼ (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (u)))) \in V$
39	20 35 16 17 38	ovmpod	$⊢ φ \to F N X = (u \in 1^{st} (F) (X) ⟼ (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (u))))$
40		simpr	$⊢ (φ \land u = A) \to u = A$
41	40	fveq2d	$⊢ (φ \land u = A) \to (X 2^{nd} (F) y) (g) (u) = (X 2^{nd} (F) y) (g) (A)$
42	41	mpteq2dv	$⊢ (φ \land u = A) \to (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (u)) = (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (A))$
43	42	mpteq2dv	$⊢ (φ \land u = A) \to (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (u))) = (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (A)))$
44	2	fvexi	$⊢ B \in V$
45	44	mptex	$⊢ (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (A))) \in V$
46	45	a1i	$⊢ φ \to (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (A))) \in V$
47	39 43 19 46	fvmptd	$⊢ φ \to (F N X) (A) = (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (A)))$

Metamath Proof Explorer

Theorem yonedalem4a

Proof