yonedalem22

	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$
	yonedalem22.g	$⊢ φ \to G \in (O Func S)$
	yonedalem22.p	$⊢ φ \to P \in B$
	yonedalem22.a	$⊢ φ \to A \in (F (O Nat S) G)$
	yonedalem22.k	$⊢ φ \to K \in (P Hom (C) X)$
Assertion	yonedalem22	$⊢ φ \to A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K = (P 2^{nd} (Y) X) (K) (⟨1^{st} (Y) (X), F⟩ 2^{nd} (H) ⟨1^{st} (Y) (P), 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		yonedalem22.g	$⊢ φ \to G \in (O Func S)$
19		yonedalem22.p	$⊢ φ \to P \in B$
20		yonedalem22.a	$⊢ φ \to A \in (F (O Nat S) G)$
21		yonedalem22.k	$⊢ φ \to K \in (P Hom (C) X)$
22	11	fveq2i	$⊢ 2^{nd} (Z) = 2^{nd} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)))$
23	22	oveqi	$⊢ ⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩ = ⟨F, X⟩ 2^{nd} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) ⟨G, P⟩$
24	23	oveqi	$⊢ A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K = A (⟨F, X⟩ 2^{nd} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) ⟨G, P⟩) K$
25		df-ov	$⊢ A (⟨F, X⟩ 2^{nd} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) ⟨G, P⟩) K = (⟨F, X⟩ 2^{nd} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) ⟨G, P⟩) (⟨A, K⟩)$
26	24 25	eqtri	$⊢ A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K = (⟨F, X⟩ 2^{nd} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) ⟨G, P⟩) (⟨A, K⟩)$
27		eqid	$⊢ Q \times_{c} O = Q \times_{c} O$
28	7	fucbas	$⊢ O Func S = {Base}_{Q}$
29	4 2	oppcbas	$⊢ B = {Base}_{O}$
30	27 28 29	xpcbas	$⊢ (O Func S) \times B = {Base}_{(Q \times_{c} O)}$
31		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)$
32		eqid	$⊢ oppCat (Q) \times_{c} Q = oppCat (Q) \times_{c} Q$
33	4	oppccat	$⊢ C \in Cat \to O \in Cat$
34	12 33	syl	$⊢ φ \to O \in Cat$
35	15	unssbd	$⊢ φ \to U \subseteq V$
36	13 35	ssexd	$⊢ φ \to U \in V$
37	5	setccat	$⊢ U \in V \to S \in Cat$
38	36 37	syl	$⊢ φ \to S \in Cat$
39	7 34 38	fuccat	$⊢ φ \to Q \in Cat$
40		eqid	$⊢ Q {2^{nd}}_{F} O = Q {2^{nd}}_{F} O$
41	27 39 34 40	2ndfcl	$⊢ φ \to Q {2^{nd}}_{F} O \in ((Q \times_{c} O) Func O)$
42		eqid	$⊢ oppCat (Q) = oppCat (Q)$
43		relfunc	$⊢ Rel (C Func Q)$
44	1 12 4 5 7 36 14	yoncl	$⊢ φ \to Y \in (C Func Q)$
45		1st2ndbr	$⊢ (Rel (C Func Q) \land Y \in (C Func Q)) \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
46	43 44 45	sylancr	$⊢ φ \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
47	4 42 46	funcoppc	$⊢ φ \to 1^{st} (Y) (O Func oppCat (Q)) tpos 2^{nd} (Y)$
48		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))$
49	47 48	sylib	$⊢ φ \to ⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \in (O Func oppCat (Q))$
50	41 49	cofucl	$⊢ φ \to ⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O) \in ((Q \times_{c} O) Func oppCat (Q))$
51		eqid	$⊢ Q {1^{st}}_{F} O = Q {1^{st}}_{F} O$
52	27 39 34 51	1stfcl	$⊢ φ \to Q {1^{st}}_{F} O \in ((Q \times_{c} O) Func Q)$
53	31 32 50 52	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))$
54	15	unssad	$⊢ φ \to ran {Hom}_{𝑓} (Q) \subseteq V$
55	8 42 6 39 13 54	hofcl	$⊢ φ \to H \in ((oppCat (Q) \times_{c} Q) Func T)$
56	16 17	opelxpd	$⊢ φ \to ⟨F, X⟩ \in ((O Func S) \times B)$
57	18 19	opelxpd	$⊢ φ \to ⟨G, P⟩ \in ((O Func S) \times B)$
58		eqid	$⊢ Hom (Q \times_{c} O) = Hom (Q \times_{c} O)$
59		eqid	$⊢ Hom (C) = Hom (C)$
60	59 4	oppchom	$⊢ X Hom (O) P = P Hom (C) X$
61	21 60	eleqtrrdi	$⊢ φ \to K \in (X Hom (O) P)$
62	20 61	opelxpd	$⊢ φ \to ⟨A, K⟩ \in ((F (O Nat S) G) \times (X Hom (O) P))$
63		eqid	$⊢ O Nat S = O Nat S$
64	7 63	fuchom	$⊢ O Nat S = Hom (Q)$
65		eqid	$⊢ Hom (O) = Hom (O)$
66	27 28 29 64 65 16 17 18 19 58	xpchom2	$⊢ φ \to ⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩ = (F (O Nat S) G) \times (X Hom (O) P)$
67	62 66	eleqtrrd	$⊢ φ \to ⟨A, K⟩ \in (⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩)$
68	30 53 55 56 57 58 67	cofu2	$⊢ φ \to (⟨F, X⟩ 2^{nd} (H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))) ⟨G, P⟩) (⟨A, K⟩) = (1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨F, X⟩) 2^{nd} (H) 1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨G, P⟩)) ((⟨F, X⟩ 2^{nd} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩))$
69	26 68	eqtrid	$⊢ φ \to A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K = (1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨F, X⟩) 2^{nd} (H) 1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨G, P⟩)) ((⟨F, X⟩ 2^{nd} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩))$
70	31 30 58 50 52 56	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⟩)⟩$
71	30 41 49 56	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⟩))$
72		fvex	$⊢ 1^{st} (Y) \in V$
73		fvex	$⊢ 2^{nd} (Y) \in V$
74	73	tposex	$⊢ tpos 2^{nd} (Y) \in V$
75	72 74	op1st	$⊢ 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) = 1^{st} (Y)$
76	75	a1i	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) = 1^{st} (Y)$
77	27 30 58 39 34 40 56	2ndf1	$⊢ φ \to 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) = 2^{nd} (⟨F, X⟩)$
78		op2ndg	$⊢ (F \in (O Func S) \land X \in B) \to 2^{nd} (⟨F, X⟩) = X$
79	16 17 78	syl2anc	$⊢ φ \to 2^{nd} (⟨F, X⟩) = X$
80	77 79	eqtrd	$⊢ φ \to 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) = X$
81	76 80	fveq12d	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) (1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩)) = 1^{st} (Y) (X)$
82	71 81	eqtrd	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) (⟨F, X⟩) = 1^{st} (Y) (X)$
83	27 30 58 39 34 51 56	1stf1	$⊢ φ \to 1^{st} (Q {1^{st}}_{F} O) (⟨F, X⟩) = 1^{st} (⟨F, X⟩)$
84		op1stg	$⊢ (F \in (O Func S) \land X \in B) \to 1^{st} (⟨F, X⟩) = F$
85	16 17 84	syl2anc	$⊢ φ \to 1^{st} (⟨F, X⟩) = F$
86	83 85	eqtrd	$⊢ φ \to 1^{st} (Q {1^{st}}_{F} O) (⟨F, X⟩) = F$
87	82 86	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⟩$
88	70 87	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⟩$
89	31 30 58 50 52 57	prf1	$⊢ φ \to 1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨G, P⟩) = ⟨1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) (⟨G, P⟩), 1^{st} (Q {1^{st}}_{F} O) (⟨G, P⟩)⟩$
90	30 41 49 57	cofu1	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) (⟨G, P⟩) = 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) (1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩))$
91	27 30 58 39 34 40 57	2ndf1	$⊢ φ \to 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩) = 2^{nd} (⟨G, P⟩)$
92		op2ndg	$⊢ (G \in (O Func S) \land P \in B) \to 2^{nd} (⟨G, P⟩) = P$
93	18 19 92	syl2anc	$⊢ φ \to 2^{nd} (⟨G, P⟩) = P$
94	91 93	eqtrd	$⊢ φ \to 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩) = P$
95	76 94	fveq12d	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) (1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩)) = 1^{st} (Y) (P)$
96	90 95	eqtrd	$⊢ φ \to 1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) (⟨G, P⟩) = 1^{st} (Y) (P)$
97	27 30 58 39 34 51 57	1stf1	$⊢ φ \to 1^{st} (Q {1^{st}}_{F} O) (⟨G, P⟩) = 1^{st} (⟨G, P⟩)$
98		op1stg	$⊢ (G \in (O Func S) \land P \in B) \to 1^{st} (⟨G, P⟩) = G$
99	18 19 98	syl2anc	$⊢ φ \to 1^{st} (⟨G, P⟩) = G$
100	97 99	eqtrd	$⊢ φ \to 1^{st} (Q {1^{st}}_{F} O) (⟨G, P⟩) = G$
101	96 100	opeq12d	$⊢ φ \to ⟨1^{st} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) (⟨G, P⟩), 1^{st} (Q {1^{st}}_{F} O) (⟨G, P⟩)⟩ = ⟨1^{st} (Y) (P), G⟩$
102	89 101	eqtrd	$⊢ φ \to 1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨G, P⟩) = ⟨1^{st} (Y) (P), G⟩$
103	88 102	oveq12d	$⊢ φ \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⟩) 2^{nd} (H) 1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨G, P⟩) = ⟨1^{st} (Y) (X), F⟩ 2^{nd} (H) ⟨1^{st} (Y) (P), G⟩$
104	31 30 58 50 52 56 57 67	prf2	$⊢ φ \to (⟨F, X⟩ 2^{nd} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩) = ⟨(⟨F, X⟩ 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩), (⟨F, X⟩ 2^{nd} (Q {1^{st}}_{F} O) ⟨G, P⟩) (⟨A, K⟩)⟩$
105	30 41 49 56 57 58 67	cofu2	$⊢ φ \to (⟨F, X⟩ 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩) = (1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩)) ((⟨F, X⟩ 2^{nd} (Q {2^{nd}}_{F} O) ⟨G, P⟩) (⟨A, K⟩))$
106	72 74	op2nd	$⊢ 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) = tpos 2^{nd} (Y)$
107	106	oveqi	$⊢ 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩) = 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) tpos 2^{nd} (Y) 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩)$
108		ovtpos	$⊢ 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) tpos 2^{nd} (Y) 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩) = 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩) 2^{nd} (Y) 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩)$
109	107 108	eqtri	$⊢ 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩) = 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩) 2^{nd} (Y) 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩)$
110	94 80	oveq12d	$⊢ φ \to 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩) 2^{nd} (Y) 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) = P 2^{nd} (Y) X$
111	109 110	eqtrid	$⊢ φ \to 1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩) = P 2^{nd} (Y) X$
112	27 30 58 39 34 40 56 57	2ndf2	$⊢ φ \to ⟨F, X⟩ 2^{nd} (Q {2^{nd}}_{F} O) ⟨G, P⟩ = {2^{nd} ↾}_{(⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩)}$
113	112	fveq1d	$⊢ φ \to (⟨F, X⟩ 2^{nd} (Q {2^{nd}}_{F} O) ⟨G, P⟩) (⟨A, K⟩) = ({2^{nd} ↾}_{(⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩)}) (⟨A, K⟩)$
114	67	fvresd	$⊢ φ \to ({2^{nd} ↾}_{(⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩)}) (⟨A, K⟩) = 2^{nd} (⟨A, K⟩)$
115		op2ndg	$⊢ (A \in (F (O Nat S) G) \land K \in (P Hom (C) X)) \to 2^{nd} (⟨A, K⟩) = K$
116	20 21 115	syl2anc	$⊢ φ \to 2^{nd} (⟨A, K⟩) = K$
117	113 114 116	3eqtrd	$⊢ φ \to (⟨F, X⟩ 2^{nd} (Q {2^{nd}}_{F} O) ⟨G, P⟩) (⟨A, K⟩) = K$
118	111 117	fveq12d	$⊢ φ \to (1^{st} (Q {2^{nd}}_{F} O) (⟨F, X⟩) 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩) 1^{st} (Q {2^{nd}}_{F} O) (⟨G, P⟩)) ((⟨F, X⟩ 2^{nd} (Q {2^{nd}}_{F} O) ⟨G, P⟩) (⟨A, K⟩)) = (P 2^{nd} (Y) X) (K)$
119	105 118	eqtrd	$⊢ φ \to (⟨F, X⟩ 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩) = (P 2^{nd} (Y) X) (K)$
120	27 30 58 39 34 51 56 57	1stf2	$⊢ φ \to ⟨F, X⟩ 2^{nd} (Q {1^{st}}_{F} O) ⟨G, P⟩ = {1^{st} ↾}_{(⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩)}$
121	120	fveq1d	$⊢ φ \to (⟨F, X⟩ 2^{nd} (Q {1^{st}}_{F} O) ⟨G, P⟩) (⟨A, K⟩) = ({1^{st} ↾}_{(⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩)}) (⟨A, K⟩)$
122	67	fvresd	$⊢ φ \to ({1^{st} ↾}_{(⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩)}) (⟨A, K⟩) = 1^{st} (⟨A, K⟩)$
123		op1stg	$⊢ (A \in (F (O Nat S) G) \land K \in (P Hom (C) X)) \to 1^{st} (⟨A, K⟩) = A$
124	20 21 123	syl2anc	$⊢ φ \to 1^{st} (⟨A, K⟩) = A$
125	121 122 124	3eqtrd	$⊢ φ \to (⟨F, X⟩ 2^{nd} (Q {1^{st}}_{F} O) ⟨G, P⟩) (⟨A, K⟩) = A$
126	119 125	opeq12d	$⊢ φ \to ⟨(⟨F, X⟩ 2^{nd} (⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩), (⟨F, X⟩ 2^{nd} (Q {1^{st}}_{F} O) ⟨G, P⟩) (⟨A, K⟩)⟩ = ⟨(P 2^{nd} (Y) X) (K), A⟩$
127	104 126	eqtrd	$⊢ φ \to (⟨F, X⟩ 2^{nd} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩) = ⟨(P 2^{nd} (Y) X) (K), A⟩$
128	103 127	fveq12d	$⊢ φ \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⟩) 2^{nd} (H) 1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨G, P⟩)) ((⟨F, X⟩ 2^{nd} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩)) = (⟨1^{st} (Y) (X), F⟩ 2^{nd} (H) ⟨1^{st} (Y) (P), G⟩) (⟨(P 2^{nd} (Y) X) (K), A⟩)$
129		df-ov	$⊢ (P 2^{nd} (Y) X) (K) (⟨1^{st} (Y) (X), F⟩ 2^{nd} (H) ⟨1^{st} (Y) (P), G⟩) A = (⟨1^{st} (Y) (X), F⟩ 2^{nd} (H) ⟨1^{st} (Y) (P), G⟩) (⟨(P 2^{nd} (Y) X) (K), A⟩)$
130	128 129	eqtr4di	$⊢ φ \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⟩) 2^{nd} (H) 1^{st} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) (⟨G, P⟩)) ((⟨F, X⟩ 2^{nd} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O)) ⟨G, P⟩) (⟨A, K⟩)) = (P 2^{nd} (Y) X) (K) (⟨1^{st} (Y) (X), F⟩ 2^{nd} (H) ⟨1^{st} (Y) (P), G⟩) A$
131	69 130	eqtrd	$⊢ φ \to A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K = (P 2^{nd} (Y) X) (K) (⟨1^{st} (Y) (X), F⟩ 2^{nd} (H) ⟨1^{st} (Y) (P), G⟩) A$

Metamath Proof Explorer

Theorem yonedalem22

Proof