fuccocl

Description: The composition of two natural transformations is a natural transformation. Remark 6.14(a) in Adamek p. 87. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fuccocl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fuccocl.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fuccocl.x	⊢ ∙ = ( comp ‘ 𝑄 )
	fuccocl.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
	fuccocl.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
Assertion	fuccocl	⊢ ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ∈ ( 𝐹 𝑁 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		fuccocl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fuccocl.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		fuccocl.x	⊢ ∙ = ( comp ‘ 𝑄 )
4		fuccocl.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
5		fuccocl.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
8	1 2 6 7 3 4 5	fucco	⊢ ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
11	2	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
12	4 11	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
13	12	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
14		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
15	13 14	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
16	15	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
18		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
19		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
20	18 13 19	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
21	6 9 20	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
22	21	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
23	2	natrcl	⊢ ( 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) )
24	5 23	syl	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) )
25	24	simpld	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
26		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
27	18 25 26	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
28	6 9 27	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
29	28	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
30	24	simprd	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐶 Func 𝐷 ) )
31		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐻 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐻 ) )
32	18 30 31	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐻 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐻 ) )
33	6 9 32	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐻 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
34	33	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
35	2 4	nat1st2nd	⊢ ( 𝜑 → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
38	2 36 6 10 37	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
39	2 5	nat1st2nd	⊢ ( 𝜑 → 𝑆 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑆 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
41	2 40 6 10 37	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
42	9 10 7 17 22 29 34 38 41	catcocl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
43	42	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
44		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
45		mptelixpg	⊢ ( ( Base ‘ 𝐶 ) ∈ V → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ) )
46	44 45	ax-mp	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
47	43 46	sylibr	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
48	8 47	eqeltrd	⊢ ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
49	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝐷 ∈ Cat )
50	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
51		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
52	50 51	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
53		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
54	50 53	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
55	28	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
56	55 53	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
57		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
58	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
59	6 57 10 58 51 53	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
60		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
61	59 60	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
62	35	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
63	2 62 6 10 53	natcl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 𝑅 ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
64	33	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 1^st ‘ 𝐻 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
65	64 53	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
66	39	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑆 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
67	2 66 6 10 53	natcl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 𝑆 ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) )
68	9 10 7 49 52 54 56 61 63 65 67	catass	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑅 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ) )
69	2 62 6 57 7 51 53 60	nati	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑅 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑥 ) ) )
70	69	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑅 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ) = ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
71	55 51	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
72	2 62 6 10 51	natcl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
73	27	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
74	6 57 10 73 51 53	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
75	74 60	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
76	9 10 7 49 52 71 56 72 75 65 67	catass	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
77	2 66 6 57 7 51 53 60	nati	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑆 ‘ 𝑥 ) ) )
78	77	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑆 ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑥 ) ) )
79	70 76 78	3eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑅 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ) = ( ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑆 ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑥 ) ) )
80	64 51	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
81	2 66 6 10 51	natcl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
82	32	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 1^st ‘ 𝐻 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐻 ) )
83	6 57 10 82 51 53	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) )
84	83 60	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) )
85	9 10 7 49 52 71 80 72 81 65 84	catass	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑆 ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
86	68 79 85	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
87	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
88	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
89	1 2 6 7 3 87 88 53	fuccoval	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑦 ) = ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑦 ) ) )
90	89	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑆 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( 𝑅 ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
91	1 2 6 7 3 87 88 51	fuccoval	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) )
92	91	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
93	86 90 92	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) ) )
94	93	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) ) )
95	2 6 57 10 7 13 30	isnat2	⊢ ( 𝜑 → ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ∈ ( 𝐹 𝑁 𝐻 ) ↔ ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐻 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑦 ) ) ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) ) ) ) )
96	48 94 95	mpbir2and	⊢ ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ∈ ( 𝐹 𝑁 𝐻 ) )

Metamath Proof Explorer

Theorem fuccocl

Proof