yonedalem3b

	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)$
	yonedalem3.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	yonedalem3b	$⊢ φ \to (G M P) (⟨F 1^{st} (Z) X, G 1^{st} (Z) P⟩ comp (T) (G 1^{st} (E) P)) (A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K) = (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K) (⟨F 1^{st} (Z) X, F 1^{st} (E) X⟩ comp (T) (G 1^{st} (E) P)) (F M 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		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		yonedalem3.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))))$
23		oveq2	$⊢ b = a \to A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b = A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a$
24	23	oveq1d	$⊢ b = a \to (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K) = (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)$
25	24	fveq1d	$⊢ b = a \to ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) = ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P)$
26	25	fveq1d	$⊢ b = a \to ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P)) = ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P))$
27	26	cbvmptv	$⊢ (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P))) = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P)))$
28		eqid	$⊢ O Nat S = O Nat S$
29	4 2	oppcbas	$⊢ B = {Base}_{O}$
30		eqid	$⊢ comp (S) = comp (S)$
31		eqid	$⊢ comp (Q) = comp (Q)$
32		eqid	$⊢ Hom (C) = Hom (C)$
33	7 28	fuchom	$⊢ O Nat S = Hom (Q)$
34		relfunc	$⊢ Rel (C Func Q)$
35	15	unssbd	$⊢ φ \to U \subseteq V$
36	13 35	ssexd	$⊢ φ \to U \in V$
37	1 12 4 5 7 36 14	yoncl	$⊢ φ \to Y \in (C Func Q)$
38		1st2ndbr	$⊢ (Rel (C Func Q) \land Y \in (C Func Q)) \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
39	34 37 38	sylancr	$⊢ φ \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
40	2 32 33 39 19 17	funcf2	$⊢ φ \to (P 2^{nd} (Y) X) : P Hom (C) X ⟶ 1^{st} (Y) (P) (O Nat S) 1^{st} (Y) (X)$
41	40 21	ffvelcdmd	$⊢ φ \to (P 2^{nd} (Y) X) (K) \in (1^{st} (Y) (P) (O Nat S) 1^{st} (Y) (X))$
42	41	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (P 2^{nd} (Y) X) (K) \in (1^{st} (Y) (P) (O Nat S) 1^{st} (Y) (X))$
43		simpr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a \in (1^{st} (Y) (X) (O Nat S) F)$
44	20	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to A \in (F (O Nat S) G)$
45	7 28 31 43 44	fuccocl	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a \in (1^{st} (Y) (X) (O Nat S) G)$
46	19	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to P \in B$
47	7 28 29 30 31 42 45 46	fuccoval	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) = (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (P) (⟨1^{st} (1^{st} (Y) (P)) (P), 1^{st} (1^{st} (Y) (X)) (P)⟩ comp (S) 1^{st} (G) (P)) (P 2^{nd} (Y) X) (K) (P)$
48	7 28 29 30 31 43 44 46	fuccoval	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (P) = A (P) (⟨1^{st} (1^{st} (Y) (X)) (P), 1^{st} (F) (P)⟩ comp (S) 1^{st} (G) (P)) a (P)$
49	36	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to U \in V$
50		eqid	$⊢ {Base}_{S} = {Base}_{S}$
51		relfunc	$⊢ Rel (O Func S)$
52	7	fucbas	$⊢ O Func S = {Base}_{Q}$
53	2 52 39	funcf1	$⊢ φ \to 1^{st} (Y) : B ⟶ O Func S$
54	53 17	ffvelcdmd	$⊢ φ \to 1^{st} (Y) (X) \in (O Func S)$
55		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))$
56	51 54 55	sylancr	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) (O Func S) 2^{nd} (1^{st} (Y) (X))$
57	29 50 56	funcf1	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) : B ⟶ {Base}_{S}$
58	5 36	setcbas	$⊢ φ \to U = {Base}_{S}$
59	58	feq3d	$⊢ φ \to (1^{st} (1^{st} (Y) (X)) : B ⟶ U \leftrightarrow 1^{st} (1^{st} (Y) (X)) : B ⟶ {Base}_{S})$
60	57 59	mpbird	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) : B ⟶ U$
61	60 19	ffvelcdmd	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) (P) \in U$
62	61	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to 1^{st} (1^{st} (Y) (X)) (P) \in U$
63		1st2ndbr	$⊢ (Rel (O Func S) \land F \in (O Func S)) \to 1^{st} (F) (O Func S) 2^{nd} (F)$
64	51 16 63	sylancr	$⊢ φ \to 1^{st} (F) (O Func S) 2^{nd} (F)$
65	29 50 64	funcf1	$⊢ φ \to 1^{st} (F) : B ⟶ {Base}_{S}$
66	58	feq3d	$⊢ φ \to (1^{st} (F) : B ⟶ U \leftrightarrow 1^{st} (F) : B ⟶ {Base}_{S})$
67	65 66	mpbird	$⊢ φ \to 1^{st} (F) : B ⟶ U$
68	67 19	ffvelcdmd	$⊢ φ \to 1^{st} (F) (P) \in U$
69	68	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to 1^{st} (F) (P) \in U$
70		1st2ndbr	$⊢ (Rel (O Func S) \land G \in (O Func S)) \to 1^{st} (G) (O Func S) 2^{nd} (G)$
71	51 18 70	sylancr	$⊢ φ \to 1^{st} (G) (O Func S) 2^{nd} (G)$
72	29 50 71	funcf1	$⊢ φ \to 1^{st} (G) : B ⟶ {Base}_{S}$
73	72 19	ffvelcdmd	$⊢ φ \to 1^{st} (G) (P) \in {Base}_{S}$
74	73 58	eleqtrrd	$⊢ φ \to 1^{st} (G) (P) \in U$
75	74	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to 1^{st} (G) (P) \in U$
76	28 43	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)⟩)$
77		eqid	$⊢ Hom (S) = Hom (S)$
78	28 76 29 77 46	natcl	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (P) \in (1^{st} (1^{st} (Y) (X)) (P) Hom (S) 1^{st} (F) (P))$
79	5 49 77 62 69	elsetchom	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (a (P) \in (1^{st} (1^{st} (Y) (X)) (P) Hom (S) 1^{st} (F) (P)) \leftrightarrow a (P) : 1^{st} (1^{st} (Y) (X)) (P) ⟶ 1^{st} (F) (P))$
80	78 79	mpbid	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (P) : 1^{st} (1^{st} (Y) (X)) (P) ⟶ 1^{st} (F) (P)$
81	28 20	nat1st2nd	$⊢ φ \to A \in (⟨1^{st} (F), 2^{nd} (F)⟩ (O Nat S) ⟨1^{st} (G), 2^{nd} (G)⟩)$
82	28 81 29 77 19	natcl	$⊢ φ \to A (P) \in (1^{st} (F) (P) Hom (S) 1^{st} (G) (P))$
83	5 36 77 68 74	elsetchom	$⊢ φ \to (A (P) \in (1^{st} (F) (P) Hom (S) 1^{st} (G) (P)) \leftrightarrow A (P) : 1^{st} (F) (P) ⟶ 1^{st} (G) (P))$
84	82 83	mpbid	$⊢ φ \to A (P) : 1^{st} (F) (P) ⟶ 1^{st} (G) (P)$
85	84	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to A (P) : 1^{st} (F) (P) ⟶ 1^{st} (G) (P)$
86	5 49 30 62 69 75 80 85	setcco	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to A (P) (⟨1^{st} (1^{st} (Y) (X)) (P), 1^{st} (F) (P)⟩ comp (S) 1^{st} (G) (P)) a (P) = A (P) \circ a (P)$
87	48 86	eqtrd	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (P) = A (P) \circ a (P)$
88	87	oveq1d	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (P) (⟨1^{st} (1^{st} (Y) (P)) (P), 1^{st} (1^{st} (Y) (X)) (P)⟩ comp (S) 1^{st} (G) (P)) (P 2^{nd} (Y) X) (K) (P) = (A (P) \circ a (P)) (⟨1^{st} (1^{st} (Y) (P)) (P), 1^{st} (1^{st} (Y) (X)) (P)⟩ comp (S) 1^{st} (G) (P)) (P 2^{nd} (Y) X) (K) (P)$
89	53 19	ffvelcdmd	$⊢ φ \to 1^{st} (Y) (P) \in (O Func S)$
90		1st2ndbr	$⊢ (Rel (O Func S) \land 1^{st} (Y) (P) \in (O Func S)) \to 1^{st} (1^{st} (Y) (P)) (O Func S) 2^{nd} (1^{st} (Y) (P))$
91	51 89 90	sylancr	$⊢ φ \to 1^{st} (1^{st} (Y) (P)) (O Func S) 2^{nd} (1^{st} (Y) (P))$
92	29 50 91	funcf1	$⊢ φ \to 1^{st} (1^{st} (Y) (P)) : B ⟶ {Base}_{S}$
93	92 19	ffvelcdmd	$⊢ φ \to 1^{st} (1^{st} (Y) (P)) (P) \in {Base}_{S}$
94	93 58	eleqtrrd	$⊢ φ \to 1^{st} (1^{st} (Y) (P)) (P) \in U$
95	94	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to 1^{st} (1^{st} (Y) (P)) (P) \in U$
96	28 41	nat1st2nd	$⊢ φ \to (P 2^{nd} (Y) X) (K) \in (⟨1^{st} (1^{st} (Y) (P)), 2^{nd} (1^{st} (Y) (P))⟩ (O Nat S) ⟨1^{st} (1^{st} (Y) (X)), 2^{nd} (1^{st} (Y) (X))⟩)$
97	28 96 29 77 19	natcl	$⊢ φ \to (P 2^{nd} (Y) X) (K) (P) \in (1^{st} (1^{st} (Y) (P)) (P) Hom (S) 1^{st} (1^{st} (Y) (X)) (P))$
98	5 36 77 94 61	elsetchom	$⊢ φ \to ((P 2^{nd} (Y) X) (K) (P) \in (1^{st} (1^{st} (Y) (P)) (P) Hom (S) 1^{st} (1^{st} (Y) (X)) (P)) \leftrightarrow (P 2^{nd} (Y) X) (K) (P) : 1^{st} (1^{st} (Y) (P)) (P) ⟶ 1^{st} (1^{st} (Y) (X)) (P))$
99	97 98	mpbid	$⊢ φ \to (P 2^{nd} (Y) X) (K) (P) : 1^{st} (1^{st} (Y) (P)) (P) ⟶ 1^{st} (1^{st} (Y) (X)) (P)$
100	99	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (P 2^{nd} (Y) X) (K) (P) : 1^{st} (1^{st} (Y) (P)) (P) ⟶ 1^{st} (1^{st} (Y) (X)) (P)$
101		fco	$⊢ (A (P) : 1^{st} (F) (P) ⟶ 1^{st} (G) (P) \land a (P) : 1^{st} (1^{st} (Y) (X)) (P) ⟶ 1^{st} (F) (P)) \to (A (P) \circ a (P)) : 1^{st} (1^{st} (Y) (X)) (P) ⟶ 1^{st} (G) (P)$
102	85 80 101	syl2anc	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (A (P) \circ a (P)) : 1^{st} (1^{st} (Y) (X)) (P) ⟶ 1^{st} (G) (P)$
103	5 49 30 95 62 75 100 102	setcco	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (A (P) \circ a (P)) (⟨1^{st} (1^{st} (Y) (P)) (P), 1^{st} (1^{st} (Y) (X)) (P)⟩ comp (S) 1^{st} (G) (P)) (P 2^{nd} (Y) X) (K) (P) = (A (P) \circ a (P)) \circ (P 2^{nd} (Y) X) (K) (P)$
104	47 88 103	3eqtrd	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) = (A (P) \circ a (P)) \circ (P 2^{nd} (Y) X) (K) (P)$
105	104	fveq1d	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P)) = ((A (P) \circ a (P)) \circ (P 2^{nd} (Y) X) (K) (P)) (\underset{˙}{1} (P))$
106	2 32 3 12 19	catidcl	$⊢ φ \to \underset{˙}{1} (P) \in (P Hom (C) P)$
107	1 2 12 19 32 19	yon11	$⊢ φ \to 1^{st} (1^{st} (Y) (P)) (P) = P Hom (C) P$
108	106 107	eleqtrrd	$⊢ φ \to \underset{˙}{1} (P) \in 1^{st} (1^{st} (Y) (P)) (P)$
109	108	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to \underset{˙}{1} (P) \in 1^{st} (1^{st} (Y) (P)) (P)$
110		fvco3	$⊢ ((P 2^{nd} (Y) X) (K) (P) : 1^{st} (1^{st} (Y) (P)) (P) ⟶ 1^{st} (1^{st} (Y) (X)) (P) \land \underset{˙}{1} (P) \in 1^{st} (1^{st} (Y) (P)) (P)) \to ((A (P) \circ a (P)) \circ (P 2^{nd} (Y) X) (K) (P)) (\underset{˙}{1} (P)) = (A (P) \circ a (P)) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P)))$
111	100 109 110	syl2anc	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to ((A (P) \circ a (P)) \circ (P 2^{nd} (Y) X) (K) (P)) (\underset{˙}{1} (P)) = (A (P) \circ a (P)) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P)))$
112	100 109	ffvelcdmd	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P)) \in 1^{st} (1^{st} (Y) (X)) (P)$
113		fvco3	$⊢ (a (P) : 1^{st} (1^{st} (Y) (X)) (P) ⟶ 1^{st} (F) (P) \land (P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P)) \in 1^{st} (1^{st} (Y) (X)) (P)) \to (A (P) \circ a (P)) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P))) = A (P) (a (P) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P))))$
114	80 112 113	syl2anc	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (A (P) \circ a (P)) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P))) = A (P) (a (P) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P))))$
115	12	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to C \in Cat$
116	17	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to X \in B$
117		eqid	$⊢ comp (C) = comp (C)$
118	21	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to K \in (P Hom (C) X)$
119	106	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to \underset{˙}{1} (P) \in (P Hom (C) P)$
120	1 2 115 46 32 116 117 46 118 119	yon2	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P)) = K (⟨P, P⟩ comp (C) X) \underset{˙}{1} (P)$
121	2 32 3 115 46 117 116 118	catrid	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to K (⟨P, P⟩ comp (C) X) \underset{˙}{1} (P) = K$
122	120 121	eqtrd	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P)) = K$
123	122	fveq2d	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (P) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P))) = a (P) (K)$
124		eqid	$⊢ Hom (O) = Hom (O)$
125	29 124 77 56 17 19	funcf2	$⊢ φ \to (X 2^{nd} (1^{st} (Y) (X)) P) : X Hom (O) P ⟶ 1^{st} (1^{st} (Y) (X)) (X) Hom (S) 1^{st} (1^{st} (Y) (X)) (P)$
126	32 4	oppchom	$⊢ X Hom (O) P = P Hom (C) X$
127	21 126	eleqtrrdi	$⊢ φ \to K \in (X Hom (O) P)$
128	125 127	ffvelcdmd	$⊢ φ \to (X 2^{nd} (1^{st} (Y) (X)) P) (K) \in (1^{st} (1^{st} (Y) (X)) (X) Hom (S) 1^{st} (1^{st} (Y) (X)) (P))$
129	60 17	ffvelcdmd	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) (X) \in U$
130	5 36 77 129 61	elsetchom	$⊢ φ \to ((X 2^{nd} (1^{st} (Y) (X)) P) (K) \in (1^{st} (1^{st} (Y) (X)) (X) Hom (S) 1^{st} (1^{st} (Y) (X)) (P)) \leftrightarrow (X 2^{nd} (1^{st} (Y) (X)) P) (K) : 1^{st} (1^{st} (Y) (X)) (X) ⟶ 1^{st} (1^{st} (Y) (X)) (P))$
131	128 130	mpbid	$⊢ φ \to (X 2^{nd} (1^{st} (Y) (X)) P) (K) : 1^{st} (1^{st} (Y) (X)) (X) ⟶ 1^{st} (1^{st} (Y) (X)) (P)$
132	131	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (X 2^{nd} (1^{st} (Y) (X)) P) (K) : 1^{st} (1^{st} (Y) (X)) (X) ⟶ 1^{st} (1^{st} (Y) (X)) (P)$
133	2 32 3 12 17	catidcl	$⊢ φ \to \underset{˙}{1} (X) \in (X Hom (C) X)$
134	1 2 12 17 32 17	yon11	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) (X) = X Hom (C) X$
135	133 134	eleqtrrd	$⊢ φ \to \underset{˙}{1} (X) \in 1^{st} (1^{st} (Y) (X)) (X)$
136	135	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to \underset{˙}{1} (X) \in 1^{st} (1^{st} (Y) (X)) (X)$
137		fvco3	$⊢ ((X 2^{nd} (1^{st} (Y) (X)) P) (K) : 1^{st} (1^{st} (Y) (X)) (X) ⟶ 1^{st} (1^{st} (Y) (X)) (P) \land \underset{˙}{1} (X) \in 1^{st} (1^{st} (Y) (X)) (X)) \to (a (P) \circ (X 2^{nd} (1^{st} (Y) (X)) P) (K)) (\underset{˙}{1} (X)) = a (P) ((X 2^{nd} (1^{st} (Y) (X)) P) (K) (\underset{˙}{1} (X)))$
138	132 136 137	syl2anc	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (a (P) \circ (X 2^{nd} (1^{st} (Y) (X)) P) (K)) (\underset{˙}{1} (X)) = a (P) ((X 2^{nd} (1^{st} (Y) (X)) P) (K) (\underset{˙}{1} (X)))$
139	127	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to K \in (X Hom (O) P)$
140	28 76 29 124 30 116 46 139	nati	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (P) (⟨1^{st} (1^{st} (Y) (X)) (X), 1^{st} (1^{st} (Y) (X)) (P)⟩ comp (S) 1^{st} (F) (P)) (X 2^{nd} (1^{st} (Y) (X)) P) (K) = (X 2^{nd} (F) P) (K) (⟨1^{st} (1^{st} (Y) (X)) (X), 1^{st} (F) (X)⟩ comp (S) 1^{st} (F) (P)) a (X)$
141	129	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to 1^{st} (1^{st} (Y) (X)) (X) \in U$
142	5 49 30 141 62 69 132 80	setcco	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (P) (⟨1^{st} (1^{st} (Y) (X)) (X), 1^{st} (1^{st} (Y) (X)) (P)⟩ comp (S) 1^{st} (F) (P)) (X 2^{nd} (1^{st} (Y) (X)) P) (K) = a (P) \circ (X 2^{nd} (1^{st} (Y) (X)) P) (K)$
143	67 17	ffvelcdmd	$⊢ φ \to 1^{st} (F) (X) \in U$
144	143	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to 1^{st} (F) (X) \in U$
145	28 76 29 77 116	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))$
146	5 49 77 141 144	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))$
147	145 146	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)$
148	29 124 77 64 17 19	funcf2	$⊢ φ \to (X 2^{nd} (F) P) : X Hom (O) P ⟶ 1^{st} (F) (X) Hom (S) 1^{st} (F) (P)$
149	148 127	ffvelcdmd	$⊢ φ \to (X 2^{nd} (F) P) (K) \in (1^{st} (F) (X) Hom (S) 1^{st} (F) (P))$
150	5 36 77 143 68	elsetchom	$⊢ φ \to ((X 2^{nd} (F) P) (K) \in (1^{st} (F) (X) Hom (S) 1^{st} (F) (P)) \leftrightarrow (X 2^{nd} (F) P) (K) : 1^{st} (F) (X) ⟶ 1^{st} (F) (P))$
151	149 150	mpbid	$⊢ φ \to (X 2^{nd} (F) P) (K) : 1^{st} (F) (X) ⟶ 1^{st} (F) (P)$
152	151	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (X 2^{nd} (F) P) (K) : 1^{st} (F) (X) ⟶ 1^{st} (F) (P)$
153	5 49 30 141 144 69 147 152	setcco	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (X 2^{nd} (F) P) (K) (⟨1^{st} (1^{st} (Y) (X)) (X), 1^{st} (F) (X)⟩ comp (S) 1^{st} (F) (P)) a (X) = (X 2^{nd} (F) P) (K) \circ a (X)$
154	140 142 153	3eqtr3d	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (P) \circ (X 2^{nd} (1^{st} (Y) (X)) P) (K) = (X 2^{nd} (F) P) (K) \circ a (X)$
155	154	fveq1d	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (a (P) \circ (X 2^{nd} (1^{st} (Y) (X)) P) (K)) (\underset{˙}{1} (X)) = ((X 2^{nd} (F) P) (K) \circ a (X)) (\underset{˙}{1} (X))$
156	133	adantr	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to \underset{˙}{1} (X) \in (X Hom (C) X)$
157	1 2 115 116 32 116 117 46 118 156	yon12	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (X 2^{nd} (1^{st} (Y) (X)) P) (K) (\underset{˙}{1} (X)) = \underset{˙}{1} (X) (⟨P, X⟩ comp (C) X) K$
158	2 32 3 115 46 117 116 118	catlid	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to \underset{˙}{1} (X) (⟨P, X⟩ comp (C) X) K = K$
159	157 158	eqtrd	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (X 2^{nd} (1^{st} (Y) (X)) P) (K) (\underset{˙}{1} (X)) = K$
160	159	fveq2d	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (P) ((X 2^{nd} (1^{st} (Y) (X)) P) (K) (\underset{˙}{1} (X))) = a (P) (K)$
161	138 155 160	3eqtr3d	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to ((X 2^{nd} (F) P) (K) \circ a (X)) (\underset{˙}{1} (X)) = a (P) (K)$
162		fvco3	$⊢ (a (X) : 1^{st} (1^{st} (Y) (X)) (X) ⟶ 1^{st} (F) (X) \land \underset{˙}{1} (X) \in 1^{st} (1^{st} (Y) (X)) (X)) \to ((X 2^{nd} (F) P) (K) \circ a (X)) (\underset{˙}{1} (X)) = (X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X)))$
163	147 136 162	syl2anc	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to ((X 2^{nd} (F) P) (K) \circ a (X)) (\underset{˙}{1} (X)) = (X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X)))$
164	123 161 163	3eqtr2d	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to a (P) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P))) = (X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X)))$
165	164	fveq2d	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to A (P) (a (P) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P)))) = A (P) ((X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X))))$
166	114 165	eqtrd	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to (A (P) \circ a (P)) ((P 2^{nd} (Y) X) (K) (P) (\underset{˙}{1} (P))) = A (P) ((X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X))))$
167	105 111 166	3eqtrd	$⊢ (φ \land a \in (1^{st} (Y) (X) (O Nat S) F)) \to ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P)) = A (P) ((X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X))))$
168	167	mpteq2dva	$⊢ φ \to (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) a) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P))) = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ A (P) ((X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X)))))$
169	27 168	eqtrid	$⊢ φ \to (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P))) = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ A (P) ((X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X)))))$
170		eqid	$⊢ Q \times_{c} O = Q \times_{c} O$
171	170 52 29	xpcbas	$⊢ (O Func S) \times B = {Base}_{(Q \times_{c} O)}$
172		eqid	$⊢ Hom (Q \times_{c} O) = Hom (Q \times_{c} O)$
173		eqid	$⊢ Hom (T) = Hom (T)$
174		relfunc	$⊢ Rel ((Q \times_{c} O) Func T)$
175	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	yonedalem1	$⊢ φ \to (Z \in ((Q \times_{c} O) Func T) \land E \in ((Q \times_{c} O) Func T))$
176	175	simpld	$⊢ φ \to Z \in ((Q \times_{c} O) Func T)$
177		1st2ndbr	$⊢ (Rel ((Q \times_{c} O) Func T) \land Z \in ((Q \times_{c} O) Func T)) \to 1^{st} (Z) ((Q \times_{c} O) Func T) 2^{nd} (Z)$
178	174 176 177	sylancr	$⊢ φ \to 1^{st} (Z) ((Q \times_{c} O) Func T) 2^{nd} (Z)$
179	16 17	opelxpd	$⊢ φ \to ⟨F, X⟩ \in ((O Func S) \times B)$
180	18 19	opelxpd	$⊢ φ \to ⟨G, P⟩ \in ((O Func S) \times B)$
181	171 172 173 178 179 180	funcf2	$⊢ φ \to (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) : ⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩ ⟶ 1^{st} (Z) (⟨F, X⟩) Hom (T) 1^{st} (Z) (⟨G, P⟩)$
182	170 52 29 33 124 16 17 18 19 172	xpchom2	$⊢ φ \to ⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩ = (F (O Nat S) G) \times (X Hom (O) P)$
183	126	xpeq2i	$⊢ (F (O Nat S) G) \times (X Hom (O) P) = (F (O Nat S) G) \times (P Hom (C) X)$
184	182 183	eqtrdi	$⊢ φ \to ⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩ = (F (O Nat S) G) \times (P Hom (C) X)$
185		df-ov	$⊢ F 1^{st} (Z) X = 1^{st} (Z) (⟨F, X⟩)$
186		df-ov	$⊢ G 1^{st} (Z) P = 1^{st} (Z) (⟨G, P⟩)$
187	185 186	oveq12i	$⊢ (F 1^{st} (Z) X) Hom (T) (G 1^{st} (Z) P) = 1^{st} (Z) (⟨F, X⟩) Hom (T) 1^{st} (Z) (⟨G, P⟩)$
188	187	eqcomi	$⊢ 1^{st} (Z) (⟨F, X⟩) Hom (T) 1^{st} (Z) (⟨G, P⟩) = (F 1^{st} (Z) X) Hom (T) (G 1^{st} (Z) P)$
189	188	a1i	$⊢ φ \to 1^{st} (Z) (⟨F, X⟩) Hom (T) 1^{st} (Z) (⟨G, P⟩) = (F 1^{st} (Z) X) Hom (T) (G 1^{st} (Z) P)$
190	184 189	feq23d	$⊢ φ \to ((⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) : ⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩ ⟶ 1^{st} (Z) (⟨F, X⟩) Hom (T) 1^{st} (Z) (⟨G, P⟩) \leftrightarrow (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) : (F (O Nat S) G) \times (P Hom (C) X) ⟶ (F 1^{st} (Z) X) Hom (T) (G 1^{st} (Z) P))$
191	181 190	mpbid	$⊢ φ \to (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) : (F (O Nat S) G) \times (P Hom (C) X) ⟶ (F 1^{st} (Z) X) Hom (T) (G 1^{st} (Z) P)$
192	191 20 21	fovcdmd	$⊢ φ \to A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K \in ((F 1^{st} (Z) X) Hom (T) (G 1^{st} (Z) P))$
193		eqid	$⊢ {Base}_{T} = {Base}_{T}$
194	171 193 178	funcf1	$⊢ φ \to 1^{st} (Z) : (O Func S) \times B ⟶ {Base}_{T}$
195	194 16 17	fovcdmd	$⊢ φ \to F 1^{st} (Z) X \in {Base}_{T}$
196	6 13	setcbas	$⊢ φ \to V = {Base}_{T}$
197	195 196	eleqtrrd	$⊢ φ \to F 1^{st} (Z) X \in V$
198	194 18 19	fovcdmd	$⊢ φ \to G 1^{st} (Z) P \in {Base}_{T}$
199	198 196	eleqtrrd	$⊢ φ \to G 1^{st} (Z) P \in V$
200	6 13 173 197 199	elsetchom	$⊢ φ \to (A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K \in ((F 1^{st} (Z) X) Hom (T) (G 1^{st} (Z) P)) \leftrightarrow (A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K) : F 1^{st} (Z) X ⟶ G 1^{st} (Z) P)$
201	192 200	mpbid	$⊢ φ \to (A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K) : F 1^{st} (Z) X ⟶ G 1^{st} (Z) P$
202	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	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$
203	4	oppccat	$⊢ C \in Cat \to O \in Cat$
204	12 203	syl	$⊢ φ \to O \in Cat$
205	5	setccat	$⊢ U \in V \to S \in Cat$
206	36 205	syl	$⊢ φ \to S \in Cat$
207	7 204 206	fuccat	$⊢ φ \to Q \in Cat$
208	8 207 52 33 54 16 89 18 31 41 20	hof2val	$⊢ φ \to (P 2^{nd} (Y) X) (K) (⟨1^{st} (Y) (X), F⟩ 2^{nd} (H) ⟨1^{st} (Y) (P), G⟩) A = (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K))$
209	202 208	eqtrd	$⊢ φ \to A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K = (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K))$
210	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$
211	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 18 19	yonedalem21	$⊢ φ \to G 1^{st} (Z) P = 1^{st} (Y) (P) (O Nat S) G$
212	209 210 211	feq123d	$⊢ φ \to ((A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K) : F 1^{st} (Z) X ⟶ G 1^{st} (Z) P \leftrightarrow (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) : 1^{st} (Y) (X) (O Nat S) F ⟶ 1^{st} (Y) (P) (O Nat S) G)$
213	201 212	mpbid	$⊢ φ \to (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) : 1^{st} (Y) (X) (O Nat S) F ⟶ 1^{st} (Y) (P) (O Nat S) G$
214		eqid	$⊢ (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) = (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K))$
215	214	fmpt	$⊢ \forall b \in (1^{st} (Y) (X) (O Nat S) F) (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K) \in (1^{st} (Y) (P) (O Nat S) G) \leftrightarrow (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) : 1^{st} (Y) (X) (O Nat S) F ⟶ 1^{st} (Y) (P) (O Nat S) G$
216	213 215	sylibr	$⊢ φ \to \forall b \in (1^{st} (Y) (X) (O Nat S) F) (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K) \in (1^{st} (Y) (P) (O Nat S) G)$
217	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 18 19 22	yonedalem3a	$⊢ φ \to (G M P = (a \in (1^{st} (Y) (P) (O Nat S) G) ⟼ a (P) (\underset{˙}{1} (P))) \land (G M P) : G 1^{st} (Z) P ⟶ G 1^{st} (E) P)$
218	217	simpld	$⊢ φ \to G M P = (a \in (1^{st} (Y) (P) (O Nat S) G) ⟼ a (P) (\underset{˙}{1} (P)))$
219		fveq1	$⊢ a = (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K) \to a (P) = ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P)$
220	219	fveq1d	$⊢ a = (A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K) \to a (P) (\underset{˙}{1} (P)) = ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P))$
221	216 209 218 220	fmptcof	$⊢ φ \to (G M P) \circ (A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K) = (b \in (1^{st} (Y) (X) (O Nat S) F) ⟼ ((A (⟨1^{st} (Y) (X), F⟩ comp (Q) G) b) (⟨1^{st} (Y) (P), 1^{st} (Y) (X)⟩ comp (Q) G) (P 2^{nd} (Y) X) (K)) (P) (\underset{˙}{1} (P)))$
222		eqid	$⊢ ⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩ = ⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩$
223	10 204 206 29 124 30 28 16 18 17 19 222 20 127	evlf2val	$⊢ φ \to A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K = A (P) (⟨1^{st} (F) (X), 1^{st} (F) (P)⟩ comp (S) 1^{st} (G) (P)) (X 2^{nd} (F) P) (K)$
224	5 36 30 143 68 74 151 84	setcco	$⊢ φ \to A (P) (⟨1^{st} (F) (X), 1^{st} (F) (P)⟩ comp (S) 1^{st} (G) (P)) (X 2^{nd} (F) P) (K) = A (P) \circ (X 2^{nd} (F) P) (K)$
225	223 224	eqtrd	$⊢ φ \to A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K = A (P) \circ (X 2^{nd} (F) P) (K)$
226	225	coeq1d	$⊢ φ \to (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K) \circ (F M X) = (A (P) \circ (X 2^{nd} (F) P) (K)) \circ (F M X)$
227	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 22	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)$
228	227	simprd	$⊢ φ \to (F M X) : F 1^{st} (Z) X ⟶ F 1^{st} (E) X$
229	227	simpld	$⊢ φ \to F M X = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ a (X) (\underset{˙}{1} (X)))$
230	10 204 206 29 16 17	evlf1	$⊢ φ \to F 1^{st} (E) X = 1^{st} (F) (X)$
231	229 210 230	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))$
232	228 231	mpbid	$⊢ φ \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)$
233		eqid	$⊢ (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)))$
234	233	fmpt	$⊢ \forall a \in (1^{st} (Y) (X) (O Nat S) F) a (X) (\underset{˙}{1} (X)) \in 1^{st} (F) (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)$
235	232 234	sylibr	$⊢ φ \to \forall a \in (1^{st} (Y) (X) (O Nat S) F) a (X) (\underset{˙}{1} (X)) \in 1^{st} (F) (X)$
236		fcompt	$⊢ (A (P) : 1^{st} (F) (P) ⟶ 1^{st} (G) (P) \land (X 2^{nd} (F) P) (K) : 1^{st} (F) (X) ⟶ 1^{st} (F) (P)) \to A (P) \circ (X 2^{nd} (F) P) (K) = (y \in 1^{st} (F) (X) ⟼ A (P) ((X 2^{nd} (F) P) (K) (y)))$
237	84 151 236	syl2anc	$⊢ φ \to A (P) \circ (X 2^{nd} (F) P) (K) = (y \in 1^{st} (F) (X) ⟼ A (P) ((X 2^{nd} (F) P) (K) (y)))$
238		2fveq3	$⊢ y = a (X) (\underset{˙}{1} (X)) \to A (P) ((X 2^{nd} (F) P) (K) (y)) = A (P) ((X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X))))$
239	235 229 237 238	fmptcof	$⊢ φ \to (A (P) \circ (X 2^{nd} (F) P) (K)) \circ (F M X) = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ A (P) ((X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X)))))$
240	226 239	eqtrd	$⊢ φ \to (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K) \circ (F M X) = (a \in (1^{st} (Y) (X) (O Nat S) F) ⟼ A (P) ((X 2^{nd} (F) P) (K) (a (X) (\underset{˙}{1} (X)))))$
241	169 221 240	3eqtr4d	$⊢ φ \to (G M P) \circ (A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K) = (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K) \circ (F M X)$
242		eqid	$⊢ comp (T) = comp (T)$
243	175	simprd	$⊢ φ \to E \in ((Q \times_{c} O) Func T)$
244		1st2ndbr	$⊢ (Rel ((Q \times_{c} O) Func T) \land E \in ((Q \times_{c} O) Func T)) \to 1^{st} (E) ((Q \times_{c} O) Func T) 2^{nd} (E)$
245	174 243 244	sylancr	$⊢ φ \to 1^{st} (E) ((Q \times_{c} O) Func T) 2^{nd} (E)$
246	171 193 245	funcf1	$⊢ φ \to 1^{st} (E) : (O Func S) \times B ⟶ {Base}_{T}$
247	246 18 19	fovcdmd	$⊢ φ \to G 1^{st} (E) P \in {Base}_{T}$
248	247 196	eleqtrrd	$⊢ φ \to G 1^{st} (E) P \in V$
249	217	simprd	$⊢ φ \to (G M P) : G 1^{st} (Z) P ⟶ G 1^{st} (E) P$
250	6 13 242 197 199 248 201 249	setcco	$⊢ φ \to (G M P) (⟨F 1^{st} (Z) X, G 1^{st} (Z) P⟩ comp (T) (G 1^{st} (E) P)) (A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K) = (G M P) \circ (A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K)$
251	246 16 17	fovcdmd	$⊢ φ \to F 1^{st} (E) X \in {Base}_{T}$
252	251 196	eleqtrrd	$⊢ φ \to F 1^{st} (E) X \in V$
253	171 172 173 245 179 180	funcf2	$⊢ φ \to (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) : ⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩ ⟶ 1^{st} (E) (⟨F, X⟩) Hom (T) 1^{st} (E) (⟨G, P⟩)$
254		df-ov	$⊢ F 1^{st} (E) X = 1^{st} (E) (⟨F, X⟩)$
255		df-ov	$⊢ G 1^{st} (E) P = 1^{st} (E) (⟨G, P⟩)$
256	254 255	oveq12i	$⊢ (F 1^{st} (E) X) Hom (T) (G 1^{st} (E) P) = 1^{st} (E) (⟨F, X⟩) Hom (T) 1^{st} (E) (⟨G, P⟩)$
257	256	eqcomi	$⊢ 1^{st} (E) (⟨F, X⟩) Hom (T) 1^{st} (E) (⟨G, P⟩) = (F 1^{st} (E) X) Hom (T) (G 1^{st} (E) P)$
258	257	a1i	$⊢ φ \to 1^{st} (E) (⟨F, X⟩) Hom (T) 1^{st} (E) (⟨G, P⟩) = (F 1^{st} (E) X) Hom (T) (G 1^{st} (E) P)$
259	184 258	feq23d	$⊢ φ \to ((⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) : ⟨F, X⟩ Hom (Q \times_{c} O) ⟨G, P⟩ ⟶ 1^{st} (E) (⟨F, X⟩) Hom (T) 1^{st} (E) (⟨G, P⟩) \leftrightarrow (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) : (F (O Nat S) G) \times (P Hom (C) X) ⟶ (F 1^{st} (E) X) Hom (T) (G 1^{st} (E) P))$
260	253 259	mpbid	$⊢ φ \to (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) : (F (O Nat S) G) \times (P Hom (C) X) ⟶ (F 1^{st} (E) X) Hom (T) (G 1^{st} (E) P)$
261	260 20 21	fovcdmd	$⊢ φ \to A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K \in ((F 1^{st} (E) X) Hom (T) (G 1^{st} (E) P))$
262	6 13 173 252 248	elsetchom	$⊢ φ \to (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K \in ((F 1^{st} (E) X) Hom (T) (G 1^{st} (E) P)) \leftrightarrow (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K) : F 1^{st} (E) X ⟶ G 1^{st} (E) P)$
263	261 262	mpbid	$⊢ φ \to (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K) : F 1^{st} (E) X ⟶ G 1^{st} (E) P$
264	6 13 242 197 252 248 228 263	setcco	$⊢ φ \to (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K) (⟨F 1^{st} (Z) X, F 1^{st} (E) X⟩ comp (T) (G 1^{st} (E) P)) (F M X) = (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K) \circ (F M X)$
265	241 250 264	3eqtr4d	$⊢ φ \to (G M P) (⟨F 1^{st} (Z) X, G 1^{st} (Z) P⟩ comp (T) (G 1^{st} (E) P)) (A (⟨F, X⟩ 2^{nd} (Z) ⟨G, P⟩) K) = (A (⟨F, X⟩ 2^{nd} (E) ⟨G, P⟩) K) (⟨F 1^{st} (Z) X, F 1^{st} (E) X⟩ comp (T) (G 1^{st} (E) P)) (F M X)$

Metamath Proof Explorer

Theorem yonedalem3b

Proof