yonedalem3b

	Ref	Expression
Hypotheses	yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
	yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
	yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
	yoneda.h	⊢ 𝐻 = ( Hom_F ‘ 𝑄 )
	yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×_c 𝑂 ) FuncCat 𝑇 )
	yoneda.e	⊢ 𝐸 = ( 𝑂 eval_F 𝑆 )
	yoneda.z	⊢ 𝑍 = ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) )
	yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
	yoneda.u	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
	yoneda.v	⊢ ( 𝜑 → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
	yonedalem21.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
	yonedalem21.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	yonedalem22.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑂 Func 𝑆 ) )
	yonedalem22.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	yonedalem22.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) )
	yonedalem22.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) )
	yonedalem3.m	⊢ 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) )
Assertion	yonedalem3b	⊢ ( 𝜑 → ( ( 𝐺 𝑀 𝑃 ) ( ⟨ ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) , ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ⟩ ( comp ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ) = ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ( ⟨ ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) , ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ⟩ ( comp ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) ( 𝐹 𝑀 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
4		yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
5		yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
6		yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
7		yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
8		yoneda.h	⊢ 𝐻 = ( Hom_F ‘ 𝑄 )
9		yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×_c 𝑂 ) FuncCat 𝑇 )
10		yoneda.e	⊢ 𝐸 = ( 𝑂 eval_F 𝑆 )
11		yoneda.z	⊢ 𝑍 = ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) )
12		yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13		yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
14		yoneda.u	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
15		yoneda.v	⊢ ( 𝜑 → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
16		yonedalem21.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
17		yonedalem21.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
18		yonedalem22.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑂 Func 𝑆 ) )
19		yonedalem22.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
20		yonedalem22.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) )
21		yonedalem22.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) )
22		yonedalem3.m	⊢ 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) )
23		oveq2	⊢ ( 𝑏 = 𝑎 → ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) = ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) )
24	23	oveq1d	⊢ ( 𝑏 = 𝑎 → ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) = ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) )
25	24	fveq1d	⊢ ( 𝑏 = 𝑎 → ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) = ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) )
26	25	fveq1d	⊢ ( 𝑏 = 𝑎 → ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) = ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) )
27	26	cbvmptv	⊢ ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) )
28		eqid	⊢ ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 )
29	4 2	oppcbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
30		eqid	⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
31		eqid	⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 )
32		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
33	7 28	fuchom	⊢ ( 𝑂 Nat 𝑆 ) = ( Hom ‘ 𝑄 )
34		relfunc	⊢ Rel ( 𝐶 Func 𝑄 )
35	15	unssbd	⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
36	13 35	ssexd	⊢ ( 𝜑 → 𝑈 ∈ V )
37	1 12 4 5 7 36 14	yoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝑄 ) )
38		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
39	34 37 38	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
40	2 32 33 39 19 17	funcf2	⊢ ( 𝜑 → ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) : ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) ⟶ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
41	40 21	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
43		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )
44	20	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝐴 ∈ ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) )
45	7 28 31 43 44	fuccocl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐺 ) )
46	19	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝑃 ∈ 𝐵 )
47	7 28 29 30 31 42 45 46	fuccoval	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) = ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ‘ 𝑃 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ) )
48	7 28 29 30 31 43 44 46	fuccoval	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ‘ 𝑃 ) = ( ( 𝐴 ‘ 𝑃 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) ( 𝑎 ‘ 𝑃 ) ) )
49	36	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝑈 ∈ V )
50		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
51		relfunc	⊢ Rel ( 𝑂 Func 𝑆 )
52	7	fucbas	⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 )
53	2 52 39	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) : 𝐵 ⟶ ( 𝑂 Func 𝑆 ) )
54	53 17	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) )
55		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
56	51 54 55	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
57	29 50 56	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
58	5 36	setcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
59	58	feq3d	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ 𝑈 ↔ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) ) )
60	57 59	mpbird	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ 𝑈 )
61	60 19	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ∈ 𝑈 )
62	61	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ∈ 𝑈 )
63		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ 𝐹 ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐹 ) )
64	51 16 63	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐹 ) )
65	29 50 64	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
66	58	feq3d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝑈 ↔ ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) ) )
67	65 66	mpbird	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝑈 )
68	67 19	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑈 )
69	68	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝑈 )
70		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ 𝐺 ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ 𝐺 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐺 ) )
71	51 18 70	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐺 ) )
72	29 50 71	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
73	72 19	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ∈ ( Base ‘ 𝑆 ) )
74	73 58	eleqtrrd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝑈 )
75	74	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝑈 )
76	28 43	nat1st2nd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝑎 ∈ ( ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ⟩ ( 𝑂 Nat 𝑆 ) ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
77		eqid	⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
78	28 76 29 77 46	natcl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 𝑎 ‘ 𝑃 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) )
79	5 49 77 62 69	elsetchom	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑃 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) ↔ ( 𝑎 ‘ 𝑃 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) )
80	78 79	mpbid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 𝑎 ‘ 𝑃 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) )
81	28 20	nat1st2nd	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝑂 Nat 𝑆 ) ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
82	28 81 29 77 19	natcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑃 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) )
83	5 36 77 68 74	elsetchom	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑃 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) ↔ ( 𝐴 ‘ 𝑃 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) )
84	82 83	mpbid	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑃 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) )
85	84	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 𝐴 ‘ 𝑃 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) )
86	5 49 30 62 69 75 80 85	setcco	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝐴 ‘ 𝑃 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) ( 𝑎 ‘ 𝑃 ) ) = ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) )
87	48 86	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ‘ 𝑃 ) = ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) )
88	87	oveq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ‘ 𝑃 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ) = ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ) )
89	53 19	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ∈ ( 𝑂 Func 𝑆 ) )
90		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) )
91	51 89 90	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) )
92	29 50 91	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
93	92 19	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ∈ ( Base ‘ 𝑆 ) )
94	93 58	eleqtrrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ∈ 𝑈 )
95	94	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ∈ 𝑈 )
96	28 41	nat1st2nd	⊢ ( 𝜑 → ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ∈ ( ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ⟩ ( 𝑂 Nat 𝑆 ) ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ⟩ ) )
97	28 96 29 77 19	natcl	⊢ ( 𝜑 → ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ) )
98	5 36 77 94 61	elsetchom	⊢ ( 𝜑 → ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ) ↔ ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ) )
99	97 98	mpbid	⊢ ( 𝜑 → ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) )
100	99	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) )
101		fco	⊢ ( ( ( 𝐴 ‘ 𝑃 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ∧ ( 𝑎 ‘ 𝑃 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) → ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) )
102	85 80 101	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) )
103	5 49 30 95 62 75 100 102	setcco	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ) = ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ∘ ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ) )
104	47 88 103	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) = ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ∘ ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ) )
105	104	fveq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) = ( ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ∘ ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ) ‘ ( 1 ‘ 𝑃 ) ) )
106	2 32 3 12 19	catidcl	⊢ ( 𝜑 → ( 1 ‘ 𝑃 ) ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑃 ) )
107	1 2 12 19 32 19	yon11	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) = ( 𝑃 ( Hom ‘ 𝐶 ) 𝑃 ) )
108	106 107	eleqtrrd	⊢ ( 𝜑 → ( 1 ‘ 𝑃 ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) )
109	108	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 1 ‘ 𝑃 ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) )
110		fvco3	⊢ ( ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ∧ ( 1 ‘ 𝑃 ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ) ‘ 𝑃 ) ) → ( ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ∘ ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ) ‘ ( 1 ‘ 𝑃 ) ) = ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) )
111	100 109 110	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ∘ ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ) ‘ ( 1 ‘ 𝑃 ) ) = ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) )
112	100 109	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) )
113		fvco3	⊢ ( ( ( 𝑎 ‘ 𝑃 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ∧ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ) → ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) = ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( 𝑎 ‘ 𝑃 ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) ) )
114	80 112 113	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) = ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( 𝑎 ‘ 𝑃 ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) ) )
115	12	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝐶 ∈ Cat )
116	17	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝑋 ∈ 𝐵 )
117		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
118	21	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝐾 ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) )
119	106	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 1 ‘ 𝑃 ) ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑃 ) )
120	1 2 115 46 32 116 117 46 118 119	yon2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) = ( 𝐾 ( ⟨ 𝑃 , 𝑃 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 1 ‘ 𝑃 ) ) )
121	2 32 3 115 46 117 116 118	catrid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 𝐾 ( ⟨ 𝑃 , 𝑃 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 1 ‘ 𝑃 ) ) = 𝐾 )
122	120 121	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) = 𝐾 )
123	122	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑃 ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) = ( ( 𝑎 ‘ 𝑃 ) ‘ 𝐾 ) )
124		eqid	⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
125	29 124 77 56 17 19	funcf2	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) ⟶ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ) )
126	32 4	oppchom	⊢ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) = ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 )
127	21 126	eleqtrrdi	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) )
128	125 127	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ) )
129	60 17	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ∈ 𝑈 )
130	5 36 77 129 61	elsetchom	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ) ↔ ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ) )
131	128 130	mpbid	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) )
132	131	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) )
133	2 32 3 12 17	catidcl	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
134	1 2 12 17 32 17	yon11	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
135	133 134	eleqtrrd	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) )
136	135	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 1 ‘ 𝑋 ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) )
137		fvco3	⊢ ( ( ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ∧ ( 1 ‘ 𝑋 ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ) → ( ( ( 𝑎 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ) ‘ ( 1 ‘ 𝑋 ) ) = ( ( 𝑎 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ‘ ( 1 ‘ 𝑋 ) ) ) )
138	132 136 137	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝑎 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ) ‘ ( 1 ‘ 𝑋 ) ) = ( ( 𝑎 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ‘ ( 1 ‘ 𝑋 ) ) ) )
139	127	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → 𝐾 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) )
140	28 76 29 124 30 116 46 139	nati	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑃 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) ( 𝑎 ‘ 𝑋 ) ) )
141	129	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ∈ 𝑈 )
142	5 49 30 141 62 69 132 80	setcco	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑃 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ) = ( ( 𝑎 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ) )
143	67 17	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
144	143	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
145	28 76 29 77 116	natcl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 𝑎 ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) )
146	5 49 77 141 144	elsetchom	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) ↔ ( 𝑎 ‘ 𝑋 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) )
147	145 146	mpbid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 𝑎 ‘ 𝑋 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
148	29 124 77 64 17 19	funcf2	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) )
149	148 127	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) )
150	5 36 77 143 68	elsetchom	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) ↔ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) )
151	149 150	mpbid	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) )
152	151	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) )
153	5 49 30 141 144 69 147 152	setcco	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) ( 𝑎 ‘ 𝑋 ) ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ∘ ( 𝑎 ‘ 𝑋 ) ) )
154	140 142 153	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ∘ ( 𝑎 ‘ 𝑋 ) ) )
155	154	fveq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝑎 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ) ‘ ( 1 ‘ 𝑋 ) ) = ( ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ∘ ( 𝑎 ‘ 𝑋 ) ) ‘ ( 1 ‘ 𝑋 ) ) )
156	133	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
157	1 2 115 116 32 116 117 46 118 156	yon12	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ‘ ( 1 ‘ 𝑋 ) ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑃 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐾 ) )
158	2 32 3 115 46 117 116 118	catlid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑃 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐾 ) = 𝐾 )
159	157 158	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ‘ ( 1 ‘ 𝑋 ) ) = 𝐾 )
160	159	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑃 ) ‘ 𝐾 ) ‘ ( 1 ‘ 𝑋 ) ) ) = ( ( 𝑎 ‘ 𝑃 ) ‘ 𝐾 ) )
161	138 155 160	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ∘ ( 𝑎 ‘ 𝑋 ) ) ‘ ( 1 ‘ 𝑋 ) ) = ( ( 𝑎 ‘ 𝑃 ) ‘ 𝐾 ) )
162		fvco3	⊢ ( ( ( 𝑎 ‘ 𝑋 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∧ ( 1 ‘ 𝑋 ) ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑋 ) ) → ( ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ∘ ( 𝑎 ‘ 𝑋 ) ) ‘ ( 1 ‘ 𝑋 ) ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) )
163	147 136 162	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ∘ ( 𝑎 ‘ 𝑋 ) ) ‘ ( 1 ‘ 𝑋 ) ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) )
164	123 161 163	3eqtr2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝑎 ‘ 𝑃 ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) )
165	164	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( 𝑎 ‘ 𝑃 ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) ) = ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ) )
166	114 165	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( 𝑎 ‘ 𝑃 ) ) ‘ ( ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) = ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ) )
167	105 111 166	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) → ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) = ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ) )
168	167	mpteq2dva	⊢ ( 𝜑 → ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑎 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ) ) )
169	27 168	eqtrid	⊢ ( 𝜑 → ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ) ) )
170		eqid	⊢ ( 𝑄 ×_c 𝑂 ) = ( 𝑄 ×_c 𝑂 )
171	170 52 29	xpcbas	⊢ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) = ( Base ‘ ( 𝑄 ×_c 𝑂 ) )
172		eqid	⊢ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) = ( Hom ‘ ( 𝑄 ×_c 𝑂 ) )
173		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
174		relfunc	⊢ Rel ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 )
175	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	yonedalem1	⊢ ( 𝜑 → ( 𝑍 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ) )
176	175	simpld	⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) )
177		1st2ndbr	⊢ ( ( Rel ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ∧ 𝑍 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ) → ( 1^st ‘ 𝑍 ) ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ( 2^nd ‘ 𝑍 ) )
178	174 176 177	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑍 ) ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ( 2^nd ‘ 𝑍 ) )
179	16 17	opelxpd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝑋 ⟩ ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
180	18 19	opelxpd	⊢ ( 𝜑 → ⟨ 𝐺 , 𝑃 ⟩ ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
181	171 172 173 178 179 180	funcf2	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) : ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) )
182	170 52 29 33 124 16 17 18 19 172	xpchom2	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) = ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) ) )
183	126	xpeq2i	⊢ ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) ) = ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) )
184	182 183	eqtrdi	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) = ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) ) )
185		df-ov	⊢ ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ )
186		df-ov	⊢ ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ )
187	185 186	oveq12i	⊢ ( ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ) = ( ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) )
188	187	eqcomi	⊢ ( ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) )
189	188	a1i	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ) )
190	184 189	feq23d	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) : ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) ↔ ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) : ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) ) ⟶ ( ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ) ) )
191	181 190	mpbid	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) : ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) ) ⟶ ( ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ) )
192	191 20 21	fovrnd	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ∈ ( ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ) )
193		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
194	171 193 178	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑍 ) : ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ⟶ ( Base ‘ 𝑇 ) )
195	194 16 17	fovrnd	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ∈ ( Base ‘ 𝑇 ) )
196	6 13	setcbas	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑇 ) )
197	195 196	eleqtrrd	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ∈ 𝑉 )
198	194 18 19	fovrnd	⊢ ( 𝜑 → ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ∈ ( Base ‘ 𝑇 ) )
199	198 196	eleqtrrd	⊢ ( 𝜑 → ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ∈ 𝑉 )
200	6 13 173 197 199	elsetchom	⊢ ( 𝜑 → ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ∈ ( ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ) ↔ ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ) )
201	192 200	mpbid	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) )
202	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	yonedalem22	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( 2^nd ‘ 𝐻 ) ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ ) 𝐴 ) )
203	4	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
204	12 203	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
205	5	setccat	⊢ ( 𝑈 ∈ V → 𝑆 ∈ Cat )
206	36 205	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
207	7 204 206	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
208	8 207 52 33 54 16 89 18 31 41 20	hof2val	⊢ ( 𝜑 → ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( 2^nd ‘ 𝐻 ) ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ ) 𝐴 ) = ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ) )
209	202 208	eqtrd	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ) )
210	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	yonedalem21	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )
211	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 18 19	yonedalem21	⊢ ( 𝜑 → ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) 𝐺 ) )
212	209 210 211	feq123d	⊢ ( 𝜑 → ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ↔ ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ) : ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ⟶ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) 𝐺 ) ) )
213	201 212	mpbid	⊢ ( 𝜑 → ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ) : ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ⟶ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) 𝐺 ) )
214		eqid	⊢ ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ) = ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) )
215	214	fmpt	⊢ ( ∀ 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) 𝐺 ) ↔ ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ) : ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ⟶ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) 𝐺 ) )
216	213 215	sylibr	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) 𝐺 ) )
217	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 18 19 22	yonedalem3a	⊢ ( 𝜑 → ( ( 𝐺 𝑀 𝑃 ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) 𝐺 ) ↦ ( ( 𝑎 ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) ∧ ( 𝐺 𝑀 𝑃 ) : ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ⟶ ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) )
218	217	simpld	⊢ ( 𝜑 → ( 𝐺 𝑀 𝑃 ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) ( 𝑂 Nat 𝑆 ) 𝐺 ) ↦ ( ( 𝑎 ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) )
219		fveq1	⊢ ( 𝑎 = ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) → ( 𝑎 ‘ 𝑃 ) = ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) )
220	219	fveq1d	⊢ ( 𝑎 = ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) → ( ( 𝑎 ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) = ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) )
221	216 209 218 220	fmptcof	⊢ ( 𝜑 → ( ( 𝐺 𝑀 𝑃 ) ∘ ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ) = ( 𝑏 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( comp ‘ 𝑄 ) 𝐺 ) 𝑏 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ⟩ ( comp ‘ 𝑄 ) 𝐺 ) ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ) ‘ 𝑃 ) ‘ ( 1 ‘ 𝑃 ) ) ) )
222		eqid	⊢ ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) = ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ )
223	10 204 206 29 124 30 28 16 18 17 19 222 20 127	evlf2val	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( ( 𝐴 ‘ 𝑃 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ) )
224	5 36 30 143 68 74 151 84	setcco	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑃 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ) = ( ( 𝐴 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ) )
225	223 224	eqtrd	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( ( 𝐴 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ) )
226	225	coeq1d	⊢ ( 𝜑 → ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ∘ ( 𝐹 𝑀 𝑋 ) ) = ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ) ∘ ( 𝐹 𝑀 𝑋 ) ) )
227	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 22	yonedalem3a	⊢ ( 𝜑 → ( ( 𝐹 𝑀 𝑋 ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ∧ ( 𝐹 𝑀 𝑋 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ) )
228	227	simprd	⊢ ( 𝜑 → ( 𝐹 𝑀 𝑋 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) )
229	227	simpld	⊢ ( 𝜑 → ( 𝐹 𝑀 𝑋 ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) )
230	10 204 206 29 16 17	evlf1	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
231	229 210 230	feq123d	⊢ ( 𝜑 → ( ( 𝐹 𝑀 𝑋 ) : ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) ⟶ ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ↔ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) : ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) )
232	228 231	mpbid	⊢ ( 𝜑 → ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) : ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
233		eqid	⊢ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) )
234	233	fmpt	⊢ ( ∀ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ↔ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) : ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
235	232 234	sylibr	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
236		fcompt	⊢ ( ( ( 𝐴 ‘ 𝑃 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ⟶ ( ( 1^st ‘ 𝐺 ) ‘ 𝑃 ) ∧ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑃 ) ) → ( ( 𝐴 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ) = ( 𝑦 ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ↦ ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ 𝑦 ) ) ) )
237	84 151 236	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ) = ( 𝑦 ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ↦ ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ 𝑦 ) ) ) )
238		2fveq3	⊢ ( 𝑦 = ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) → ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ 𝑦 ) ) = ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ) )
239	235 229 237 238	fmptcof	⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝑃 ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ) ∘ ( 𝐹 𝑀 𝑋 ) ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ) ) )
240	226 239	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ∘ ( 𝐹 𝑀 𝑋 ) ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↦ ( ( 𝐴 ‘ 𝑃 ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑃 ) ‘ 𝐾 ) ‘ ( ( 𝑎 ‘ 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) ) ) ) )
241	169 221 240	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐺 𝑀 𝑃 ) ∘ ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ) = ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ∘ ( 𝐹 𝑀 𝑋 ) ) )
242		eqid	⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 )
243	175	simprd	⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) )
244		1st2ndbr	⊢ ( ( Rel ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ) → ( 1^st ‘ 𝐸 ) ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ( 2^nd ‘ 𝐸 ) )
245	174 243 244	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐸 ) ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ( 2^nd ‘ 𝐸 ) )
246	171 193 245	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐸 ) : ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ⟶ ( Base ‘ 𝑇 ) )
247	246 18 19	fovrnd	⊢ ( 𝜑 → ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ∈ ( Base ‘ 𝑇 ) )
248	247 196	eleqtrrd	⊢ ( 𝜑 → ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ∈ 𝑉 )
249	217	simprd	⊢ ( 𝜑 → ( 𝐺 𝑀 𝑃 ) : ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ⟶ ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) )
250	6 13 242 197 199 248 201 249	setcco	⊢ ( 𝜑 → ( ( 𝐺 𝑀 𝑃 ) ( ⟨ ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) , ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ⟩ ( comp ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ) = ( ( 𝐺 𝑀 𝑃 ) ∘ ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ) )
251	246 16 17	fovrnd	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ∈ ( Base ‘ 𝑇 ) )
252	251 196	eleqtrrd	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ∈ 𝑉 )
253	171 172 173 245 179 180	funcf2	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) : ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) )
254		df-ov	⊢ ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ )
255		df-ov	⊢ ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ )
256	254 255	oveq12i	⊢ ( ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) = ( ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) )
257	256	eqcomi	⊢ ( ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) )
258	257	a1i	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) )
259	184 258	feq23d	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) : ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) ↔ ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) : ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) ) ⟶ ( ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) ) )
260	253 259	mpbid	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) : ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) ) ⟶ ( ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) )
261	260 20 21	fovrnd	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ∈ ( ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) )
262	6 13 173 252 248	elsetchom	⊢ ( 𝜑 → ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ∈ ( ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ( Hom ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) ↔ ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) : ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ⟶ ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) )
263	261 262	mpbid	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) : ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ⟶ ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) )
264	6 13 242 197 252 248 228 263	setcco	⊢ ( 𝜑 → ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ( ⟨ ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) , ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ⟩ ( comp ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) ( 𝐹 𝑀 𝑋 ) ) = ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ∘ ( 𝐹 𝑀 𝑋 ) ) )
265	241 250 264	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐺 𝑀 𝑃 ) ( ⟨ ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) , ( 𝐺 ( 1^st ‘ 𝑍 ) 𝑃 ) ⟩ ( comp ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ) = ( ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) ( ⟨ ( 𝐹 ( 1^st ‘ 𝑍 ) 𝑋 ) , ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) ⟩ ( comp ‘ 𝑇 ) ( 𝐺 ( 1^st ‘ 𝐸 ) 𝑃 ) ) ( 𝐹 𝑀 𝑋 ) ) )

Metamath Proof Explorer

Theorem yonedalem3b

Proof