cofucl

Description: The composition of two functors is a functor. Proposition 3.23 of Adamek p. 33. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofucl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	cofucl.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
Assertion	cofucl	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		cofucl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
2		cofucl.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
3		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
4	3 1 2	cofuval	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )
5	3 1 2	cofu1st	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) = ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) )
6	4	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ ) )
7		fvex	⊢ ( 1^st ‘ 𝐺 ) ∈ V
8		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
9	7 8	coex	⊢ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) ∈ V
10		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
11	10 10	mpoex	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ∈ V
12	9 11	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
13	6 12	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) )
14	5 13	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) , ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ⟩ = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )
15	4 14	eqtr4d	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = ⟨ ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) , ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ⟩ )
16		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
17		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
18		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
19		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
20	18 2 19	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
21	16 17 20	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
22		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
23		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
24	22 1 23	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
25	3 16 24	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
26		fco	⊢ ( ( ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) ∧ ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
27	21 25 26	syl2anc	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
28	5	feq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) ↔ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) ) )
29	27 28	mpbird	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
30		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
31		ovex	⊢ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∈ V
32		ovex	⊢ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ∈ V
33	31 32	coex	⊢ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ∈ V
34	30 33	fnmpoi	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
35	13	fneq1d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
36	34 35	mpbiri	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
37		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
38		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
39	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
40	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
41		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
42	40 41	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
43		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
44	40 43	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
45	16 37 38 39 42 44	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
46		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
47	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
48	3 46 37 47 41 43	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
49		fco	⊢ ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ∧ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
50	45 48 49	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
51		ovex	⊢ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ∈ V
52		ovex	⊢ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∈ V
53	51 52	elmap	⊢ ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ∈ ( ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ↔ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
54	50 53	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ∈ ( ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
55	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
56	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
57	3 55 56 41 43	cofu2nd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
58	3 55 56 41	cofu1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
59	3 55 56 43	cofu1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
60	58 59	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) = ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
61	60	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
62	54 57 61	3eltr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ∈ ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
63	62	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ∈ ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
64		fveq2	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) = ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
65		df-ov	⊢ ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) = ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
66	64 65	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) = ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) )
67		vex	⊢ 𝑥 ∈ V
68		vex	⊢ 𝑦 ∈ V
69	67 68	op1std	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑧 ) = 𝑥 )
70	69	fveq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) = ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) )
71	67 68	op2ndd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑧 ) = 𝑦 )
72	71	fveq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) )
73	70 72	oveq12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) = ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) )
74		fveq2	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
75		df-ov	⊢ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
76	74 75	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
77	73 76	oveq12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) = ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
78	66 77	eleq12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ∈ ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) )
79	78	ralxp	⊢ ( ∀ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ∈ ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
80	63 79	sylibr	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
81		fvex	⊢ ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ∈ V
82	81	elixp	⊢ ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ∀ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ∈ ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ) )
83	36 80 82	sylanbrc	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
84		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
85		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
86	24	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
87		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
88	3 84 85 86 87	funcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
89	88	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
90		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
91	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
92	25	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
93	16 85 90 91 92	funcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
94	89 93	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
95	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
96	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
97		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
98	1 97	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
99	98	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
100	99	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
101	3 46 84 100 87	catidcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
102	3 95 96 87 87 46 101	cofu2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ) )
103	3 95 96 87	cofu1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
104	103	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
105	94 102 104	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ) )
106	86	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
107		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
108		simprlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
109	3 46 37 106 107 108	funcf2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
110		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
111	100	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝐶 ∈ Cat )
112		simprll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
113		simprrl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
114		simprrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
115	3 46 110 111 107 112 108 113 114	catcocl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
116		fvco3	⊢ ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) )
117	109 115 116	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) )
118		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
119	3 46 110 118 106 107 112 108 113 114	funcco	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
120	119	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ) )
121		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
122	91	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
123	92	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
124	25	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
125	124	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
126	125 112	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
127	125 108	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
128	3 46 37 106 107 112	funcf2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
129	128 113	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
130	3 46 37 106 112 108	funcf2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
131	130 114	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
132	16 37 118 121 122 123 126 127 129 131	funcco	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ) = ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ) )
133	117 120 132	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ) )
134	95	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
135	96	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
136	3 134 135 107 108	cofu2nd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ) )
137	136	fveq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) )
138	103	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
139	3 134 135 112	cofu1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
140	138 139	opeq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟩ )
141	3 134 135 108	cofu1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
142	140 141	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ) = ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ) )
143	3 134 135 112 108 46 114	cofu2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑦 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ 𝑔 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ) )
144	3 134 135 107 112 46 113	cofu2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
145	142 143 144	oveq123d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( 𝑦 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ) )
146	133 137 145	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ) )
147	146	anassrs	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ) )
148	147	ralrimivva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ) )
149	148	ralrimivva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ) )
150	105 149	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ) ) )
151	150	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ) ) )
152		funcrcl	⊢ ( 𝐺 ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
153	2 152	syl	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
154	153	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
155	3 17 46 38 84 90 110 121 99 154	isfunc	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ↔ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) ∧ ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ) ) ) ) )
156	29 83 151 155	mpbir3and	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) )
157		df-br	⊢ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ↔ ⟨ ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) , ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ⟩ ∈ ( 𝐶 Func 𝐸 ) )
158	156 157	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) , ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ⟩ ∈ ( 𝐶 Func 𝐸 ) )
159	15 158	eqeltrd	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )

Metamath Proof Explorer

Theorem cofucl

Proof