yonedalem22

	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 ‘ 𝐶 ) 𝑋 ) )
Assertion	yonedalem22	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( 2^nd ‘ 𝐻 ) ⟨ ( ( 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	11	fveq2i	⊢ ( 2^nd ‘ 𝑍 ) = ( 2^nd ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) )
23	22	oveqi	⊢ ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) = ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) ⟨ 𝐺 , 𝑃 ⟩ )
24	23	oveqi	⊢ ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 )
25		df-ov	⊢ ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ )
26	24 25	eqtri	⊢ ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ )
27		eqid	⊢ ( 𝑄 ×_c 𝑂 ) = ( 𝑄 ×_c 𝑂 )
28	7	fucbas	⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 )
29	4 2	oppcbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
30	27 28 29	xpcbas	⊢ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) = ( Base ‘ ( 𝑄 ×_c 𝑂 ) )
31		eqid	⊢ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) = ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) )
32		eqid	⊢ ( ( oppCat ‘ 𝑄 ) ×_c 𝑄 ) = ( ( oppCat ‘ 𝑄 ) ×_c 𝑄 )
33	4	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
34	12 33	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
35	15	unssbd	⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
36	13 35	ssexd	⊢ ( 𝜑 → 𝑈 ∈ V )
37	5	setccat	⊢ ( 𝑈 ∈ V → 𝑆 ∈ Cat )
38	36 37	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
39	7 34 38	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
40		eqid	⊢ ( 𝑄 2^nd_F 𝑂 ) = ( 𝑄 2^nd_F 𝑂 )
41	27 39 34 40	2ndfcl	⊢ ( 𝜑 → ( 𝑄 2^nd_F 𝑂 ) ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑂 ) )
42		eqid	⊢ ( oppCat ‘ 𝑄 ) = ( oppCat ‘ 𝑄 )
43		relfunc	⊢ Rel ( 𝐶 Func 𝑄 )
44	1 12 4 5 7 36 14	yoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝑄 ) )
45		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
46	43 44 45	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
47	4 42 46	funcoppc	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) tpos ( 2^nd ‘ 𝑌 ) )
48		df-br	⊢ ( ( 1^st ‘ 𝑌 ) ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) tpos ( 2^nd ‘ 𝑌 ) ↔ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) )
49	47 48	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) )
50	41 49	cofucl	⊢ ( 𝜑 → ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ∈ ( ( 𝑄 ×_c 𝑂 ) Func ( oppCat ‘ 𝑄 ) ) )
51		eqid	⊢ ( 𝑄 1^st_F 𝑂 ) = ( 𝑄 1^st_F 𝑂 )
52	27 39 34 51	1stfcl	⊢ ( 𝜑 → ( 𝑄 1^st_F 𝑂 ) ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑄 ) )
53	31 32 50 52	prfcl	⊢ ( 𝜑 → ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ∈ ( ( 𝑄 ×_c 𝑂 ) Func ( ( oppCat ‘ 𝑄 ) ×_c 𝑄 ) ) )
54	15	unssad	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝑄 ) ⊆ 𝑉 )
55	8 42 6 39 13 54	hofcl	⊢ ( 𝜑 → 𝐻 ∈ ( ( ( oppCat ‘ 𝑄 ) ×_c 𝑄 ) Func 𝑇 ) )
56	16 17	opelxpd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝑋 ⟩ ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
57	18 19	opelxpd	⊢ ( 𝜑 → ⟨ 𝐺 , 𝑃 ⟩ ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
58		eqid	⊢ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) = ( Hom ‘ ( 𝑄 ×_c 𝑂 ) )
59		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
60	59 4	oppchom	⊢ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) = ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 )
61	21 60	eleqtrrdi	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) )
62	20 61	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐾 ⟩ ∈ ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) ) )
63		eqid	⊢ ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 )
64	7 63	fuchom	⊢ ( 𝑂 Nat 𝑆 ) = ( Hom ‘ 𝑄 )
65		eqid	⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
66	27 28 29 64 65 16 17 18 19 58	xpchom2	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) = ( ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) × ( 𝑋 ( Hom ‘ 𝑂 ) 𝑃 ) ) )
67	62 66	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐾 ⟩ ∈ ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) )
68	30 53 55 56 57 58 67	cofu2	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ( ( ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ) )
69	26 68	eqtrid	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( ( ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ) )
70	31 30 58 50 52 56	prf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ⟨ ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) , ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ⟩ )
71	30 41 49 56	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ‘ ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ) )
72		fvex	⊢ ( 1^st ‘ 𝑌 ) ∈ V
73		fvex	⊢ ( 2^nd ‘ 𝑌 ) ∈ V
74	73	tposex	⊢ tpos ( 2^nd ‘ 𝑌 ) ∈ V
75	72 74	op1st	⊢ ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) = ( 1^st ‘ 𝑌 )
76	75	a1i	⊢ ( 𝜑 → ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) = ( 1^st ‘ 𝑌 ) )
77	27 30 58 39 34 40 56	2ndf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( 2^nd ‘ ⟨ 𝐹 , 𝑋 ⟩ ) )
78		op2ndg	⊢ ( ( 𝐹 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑋 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝑋 )
79	16 17 78	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝑋 )
80	77 79	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝑋 )
81	76 80	fveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ‘ ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) )
82	71 81	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) )
83	27 30 58 39 34 51 56	1stf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ( 1^st ‘ ⟨ 𝐹 , 𝑋 ⟩ ) )
84		op1stg	⊢ ( ( 𝐹 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑋 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝐹 )
85	16 17 84	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝐹 )
86	83 85	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = 𝐹 )
87	82 86	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) , ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ⟩ = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ )
88	70 87	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ )
89	31 30 58 50 52 57	prf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = ⟨ ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) , ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ⟩ )
90	30 41 49 57	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = ( ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ‘ ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) )
91	27 30 58 39 34 40 57	2ndf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = ( 2^nd ‘ ⟨ 𝐺 , 𝑃 ⟩ ) )
92		op2ndg	⊢ ( ( 𝐺 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑃 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = 𝑃 )
93	18 19 92	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = 𝑃 )
94	91 93	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = 𝑃 )
95	76 94	fveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ‘ ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) )
96	90 95	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) )
97	27 30 58 39 34 51 57	1stf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = ( 1^st ‘ ⟨ 𝐺 , 𝑃 ⟩ ) )
98		op1stg	⊢ ( ( 𝐺 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑃 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = 𝐺 )
99	18 19 98	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = 𝐺 )
100	97 99	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = 𝐺 )
101	96 100	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) , ( ( 1^st ‘ ( 𝑄 1^st_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ⟩ = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ )
102	89 101	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ )
103	88 102	oveq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( 2^nd ‘ 𝐻 ) ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ ) )
104	31 30 58 50 52 56 57 67	prf2	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ⟨ ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) , ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 1^st_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ⟩ )
105	30 41 49 56 57 58 67	cofu2	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ( ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 2^nd_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ) )
106	72 74	op2nd	⊢ ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) = tpos ( 2^nd ‘ 𝑌 )
107	106	oveqi	⊢ ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) tpos ( 2^nd ‘ 𝑌 ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) )
108		ovtpos	⊢ ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) tpos ( 2^nd ‘ 𝑌 ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ( 2^nd ‘ 𝑌 ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) )
109	107 108	eqtri	⊢ ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ( 2^nd ‘ 𝑌 ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) )
110	94 80	oveq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ( 2^nd ‘ 𝑌 ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ) = ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) )
111	109 110	eqtrid	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) = ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) )
112	27 30 58 39 34 40 56 57	2ndf2	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 2^nd_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) = ( 2^nd ↾ ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ) )
113	112	fveq1d	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 2^nd_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ( ( 2^nd ↾ ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) )
114	67	fvresd	⊢ ( 𝜑 → ( ( 2^nd ↾ ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ( 2^nd ‘ ⟨ 𝐴 , 𝐾 ⟩ ) )
115		op2ndg	⊢ ( ( 𝐴 ∈ ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 2^nd ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = 𝐾 )
116	20 21 115	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = 𝐾 )
117	113 114 116	3eqtrd	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 2^nd_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = 𝐾 )
118	111 117	fveq12d	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ) ( ( 1^st ‘ ( 𝑄 2^nd_F 𝑂 ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 2^nd_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ) = ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) )
119	105 118	eqtrd	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) )
120	27 30 58 39 34 51 56 57	1stf2	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 1^st_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) = ( 1^st ↾ ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ) )
121	120	fveq1d	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 1^st_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ( ( 1^st ↾ ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) )
122	67	fvresd	⊢ ( 𝜑 → ( ( 1^st ↾ ( ⟨ 𝐹 , 𝑋 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ( 1^st ‘ ⟨ 𝐴 , 𝐾 ⟩ ) )
123		op1stg	⊢ ( ( 𝐴 ∈ ( 𝐹 ( 𝑂 Nat 𝑆 ) 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 1^st ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = 𝐴 )
124	20 21 123	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = 𝐴 )
125	121 122 124	3eqtrd	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 1^st_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = 𝐴 )
126	119 125	opeq12d	⊢ ( 𝜑 → ⟨ ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) , ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( 𝑄 1^st_F 𝑂 ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ⟩ = ⟨ ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) , 𝐴 ⟩ )
127	104 126	eqtrd	⊢ ( 𝜑 → ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) = ⟨ ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) , 𝐴 ⟩ )
128	103 127	fveq12d	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ) = ( ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( 2^nd ‘ 𝐻 ) ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ ) ‘ ⟨ ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) , 𝐴 ⟩ ) )
129		df-ov	⊢ ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( 2^nd ‘ 𝐻 ) ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ ) 𝐴 ) = ( ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( 2^nd ‘ 𝐻 ) ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ ) ‘ ⟨ ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) , 𝐴 ⟩ )
130	128 129	eqtr4di	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐹 , 𝑋 ⟩ ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ‘ ⟨ 𝐺 , 𝑃 ⟩ ) ) ‘ ( ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) ) ⟨ 𝐺 , 𝑃 ⟩ ) ‘ ⟨ 𝐴 , 𝐾 ⟩ ) ) = ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( 2^nd ‘ 𝐻 ) ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ ) 𝐴 ) )
131	69 130	eqtrd	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝑋 ⟩ ( 2^nd ‘ 𝑍 ) ⟨ 𝐺 , 𝑃 ⟩ ) 𝐾 ) = ( ( ( 𝑃 ( 2^nd ‘ 𝑌 ) 𝑋 ) ‘ 𝐾 ) ( ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 ⟩ ( 2^nd ‘ 𝐻 ) ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑃 ) , 𝐺 ⟩ ) 𝐴 ) )

Metamath Proof Explorer

Theorem yonedalem22

Proof