Theorem cofucl 16371

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

Hypotheses

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

Assertion

Ref	Expression
cofucl	⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸))

Proof of Theorem cofucl

Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2610	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
2		cofucl.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		cofucl.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))
4	1, 2, 3	cofuval 16365	. . 3 ⊢ (𝜑 → (𝐺 ∘func 𝐹) = ⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩)
5	1, 2, 3	cofu1st 16366	. . . 4 ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹)) = ((1st ‘𝐺) ∘ (1st ‘𝐹)))
6	4	fveq2d 6107	. . . . 5 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) = (2nd ‘⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩))
7		fvex 6113	. . . . . . 7 ⊢ (1st ‘𝐺) ∈ V
8		fvex 6113	. . . . . . 7 ⊢ (1st ‘𝐹) ∈ V
9	7, 8	coex 7011	. . . . . 6 ⊢ ((1st ‘𝐺) ∘ (1st ‘𝐹)) ∈ V
10		fvex 6113	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
11	10, 10	mpt2ex 7136	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) ∈ V
12	9, 11	op2nd 7068	. . . . 5 ⊢ (2nd ‘⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))
13	6, 12	syl6eq 2660	. . . 4 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))))
14	5, 13	opeq12d 4348	. . 3 ⊢ (𝜑 → ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩ = ⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩)
15	4, 14	eqtr4d 2647	. 2 ⊢ (𝜑 → (𝐺 ∘func 𝐹) = ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩)
16		eqid 2610	. . . . . . 7 ⊢ (Base‘𝐷) = (Base‘𝐷)
17		eqid 2610	. . . . . . 7 ⊢ (Base‘𝐸) = (Base‘𝐸)
18		relfunc 16345	. . . . . . . 8 ⊢ Rel (𝐷 Func 𝐸)
19		1st2ndbr 7108	. . . . . . . 8 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝐺 ∈ (𝐷 Func 𝐸)) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
20	18, 3, 19	sylancr 694	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
21	16, 17, 20	funcf1 16349	. . . . . 6 ⊢ (𝜑 → (1st ‘𝐺):(Base‘𝐷)⟶(Base‘𝐸))
22		relfunc 16345	. . . . . . . 8 ⊢ Rel (𝐶 Func 𝐷)
23		1st2ndbr 7108	. . . . . . . 8 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
24	22, 2, 23	sylancr 694	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
25	1, 16, 24	funcf1 16349	. . . . . 6 ⊢ (𝜑 → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
26		fco 5971	. . . . . 6 ⊢ (((1st ‘𝐺):(Base‘𝐷)⟶(Base‘𝐸) ∧ (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) → ((1st ‘𝐺) ∘ (1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
27	21, 25, 26	syl2anc 691	. . . . 5 ⊢ (𝜑 → ((1st ‘𝐺) ∘ (1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
28	5	feq1d 5943	. . . . 5 ⊢ (𝜑 → ((1st ‘(𝐺 ∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ↔ ((1st ‘𝐺) ∘ (1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸)))
29	27, 28	mpbird 246	. . . 4 ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
30		eqid 2610	. . . . . . 7 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))
31		ovex 6577	. . . . . . . 8 ⊢ (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∈ V
32		ovex 6577	. . . . . . . 8 ⊢ (𝑥(2nd ‘𝐹)𝑦) ∈ V
33	31, 32	coex 7011	. . . . . . 7 ⊢ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ V
34	30, 33	fnmpt2i 7128	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))
35	13	fneq1d 5895	. . . . . 6 ⊢ (𝜑 → ((2nd ‘(𝐺 ∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))))
36	34, 35	mpbiri 247	. . . . 5 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)))
37		eqid 2610	. . . . . . . . . . 11 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
38		eqid 2610	. . . . . . . . . . 11 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
39	20	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
40	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
41		simprl 790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
42	40, 41	ffvelrnd 6268	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
43		simprr 792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
44	40, 43	ffvelrnd 6268	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
45	16, 37, 38, 39, 42, 44	funcf2 16351	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
46		eqid 2610	. . . . . . . . . . 11 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
47	24	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
48	1, 46, 37, 47, 41, 43	funcf2 16351	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
49		fco 5971	. . . . . . . . . 10 ⊢ (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ∧ (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
50	45, 48, 49	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
51		ovex 6577	. . . . . . . . . 10 ⊢ (((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ∈ V
52		ovex 6577	. . . . . . . . . 10 ⊢ (𝑥(Hom ‘𝐶)𝑦) ∈ V
53	51, 52	elmap 7772	. . . . . . . . 9 ⊢ (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ ((((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)) ↔ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
54	50, 53	sylibr 223	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ ((((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
55	2	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
56	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸))
57	1, 55, 56, 41, 43	cofu2nd 16368	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))
58	1, 55, 56, 41	cofu1 16367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑥) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)))
59	1, 55, 56, 43	cofu1 16367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑦) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))
60	58, 59	oveq12d 6567	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) = (((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
61	60	oveq1d 6564	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)) = ((((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
62	54, 57, 61	3eltr4d 2703	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
63	62	ralrimivva 2954	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
64		fveq2 6103	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) = ((2nd ‘(𝐺 ∘func 𝐹))‘⟨𝑥, 𝑦⟩))
65		df-ov 6552	. . . . . . . . 9 ⊢ (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) = ((2nd ‘(𝐺 ∘func 𝐹))‘⟨𝑥, 𝑦⟩)
66	64, 65	syl6eqr 2662	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) = (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦))
67		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
68		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
69	67, 68	op1std 7069	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑧) = 𝑥)
70	69	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧)) = ((1st ‘(𝐺 ∘func 𝐹))‘𝑥))
71	67, 68	op2ndd 7070	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
72	71	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧)) = ((1st ‘(𝐺 ∘func 𝐹))‘𝑦))
73	70, 72	oveq12d 6567	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) = (((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)))
74		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩))
75		df-ov 6552	. . . . . . . . . 10 ⊢ (𝑥(Hom ‘𝐶)𝑦) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩)
76	74, 75	syl6eqr 2662	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = (𝑥(Hom ‘𝐶)𝑦))
77	73, 76	oveq12d 6567	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) = ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
78	66, 77	eleq12d 2682	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ↔ (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦))))
79	78	ralxp 5185	. . . . . 6 ⊢ (∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ↔ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐶)𝑦)))
80	63, 79	sylibr 223	. . . . 5 ⊢ (𝜑 → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
81		fvex 6113	. . . . . 6 ⊢ (2nd ‘(𝐺 ∘func 𝐹)) ∈ V
82	81	elixp 7801	. . . . 5 ⊢ ((2nd ‘(𝐺 ∘func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ↔ ((2nd ‘(𝐺 ∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧))))
83	36, 80, 82	sylanbrc 695	. . . 4 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
84		eqid 2610	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
85		eqid 2610	. . . . . . . . . 10 ⊢ (Id‘𝐷) = (Id‘𝐷)
86	24	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
87		simpr 476	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
88	1, 84, 85, 86, 87	funcid 16353	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)))
89	88	fveq2d 6107	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))))
90		eqid 2610	. . . . . . . . 9 ⊢ (Id‘𝐸) = (Id‘𝐸)
91	20	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
92	25	ffvelrnda 6267	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
93	16, 85, 90, 91, 92	funcid 16353	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))))
94	89, 93	eqtrd 2644	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))))
95	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
96	3	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐷 Func 𝐸))
97		funcrcl 16346	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
98	2, 97	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
99	98	simpld 474	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ Cat)
100	99	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
101	1, 46, 84, 100, 87	catidcl 16166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
102	1, 95, 96, 87, 87, 46, 101	cofu2 16369	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))))
103	1, 95, 96, 87	cofu1 16367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑥) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)))
104	103	fveq2d 6107	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸)‘((1st ‘(𝐺 ∘func 𝐹))‘𝑥)) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))))
105	94, 102, 104	3eqtr4d 2654	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func 𝐹))‘𝑥)))
106	86	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
107		simplr 788	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ (Base‘𝐶))
108		simprlr 799	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ (Base‘𝐶))
109	1, 46, 37, 106, 107, 108	funcf2 16351	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
110		eqid 2610	. . . . . . . . . . . . 13 ⊢ (comp‘𝐶) = (comp‘𝐶)
111	100	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐶 ∈ Cat)
112		simprll 798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ (Base‘𝐶))
113		simprrl 800	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
114		simprrr 801	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
115	1, 46, 110, 111, 107, 112, 108, 113, 114	catcocl 16169	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
116		fvco3 6185	. . . . . . . . . . . 12 ⊢ (((𝑥(2nd ‘𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
117	109, 115, 116	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
118		eqid 2610	. . . . . . . . . . . . 13 ⊢ (comp‘𝐷) = (comp‘𝐷)
119	1, 46, 110, 118, 106, 107, 112, 108, 113, 114	funcco 16354	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))
120	119	fveq2d 6107	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓))))
121		eqid 2610	. . . . . . . . . . . 12 ⊢ (comp‘𝐸) = (comp‘𝐸)
122	91	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
123	92	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
124	25	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
125	124	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
126	125, 112	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
127	125, 108	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷))
128	1, 46, 37, 106, 107, 112	funcf2 16351	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
129	128, 113	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘𝐹)𝑦)‘𝑓) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
130	1, 46, 37, 106, 112, 108	funcf2 16351	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
131	130, 114	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
132	16, 37, 118, 121, 122, 123, 126, 127, 129, 131	funcco 16354	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓))) = (((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔))(⟨((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))⟩(comp‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓))))
133	117, 120, 132	3eqtrd 2648	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔))(⟨((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))⟩(comp‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓))))
134	95	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐹 ∈ (𝐶 Func 𝐷))
135	96	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐺 ∈ (𝐷 Func 𝐸))
136	1, 134, 135, 107, 108	cofu2nd 16368	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧)))
137	136	fveq1d 6105	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
138	103	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑥) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)))
139	1, 134, 135, 112	cofu1 16367	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑦) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))
140	138, 139	opeq12d 4348	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩ = ⟨((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))⟩)
141	1, 134, 135, 108	cofu1 16367	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑧) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))
142	140, 141	oveq12d 6567	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧)) = (⟨((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))⟩(comp‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧))))
143	1, 134, 135, 112, 108, 46, 114	cofu2 16369	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔) = ((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔)))
144	1, 134, 135, 107, 112, 46, 113	cofu2 16369	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))
145	142, 143, 144	oveq123d 6570	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)) = (((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔))(⟨((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))⟩(comp‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓))))
146	133, 137, 145	3eqtr4d 2654	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
147	146	anassrs 678	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
148	147	ralrimivva 2954	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
149	148	ralrimivva 2954	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
150	105, 149	jca 553	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func 𝐹))‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓))))
151	150	ralrimiva 2949	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)(((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func 𝐹))‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓))))
152		funcrcl 16346	. . . . . . 7 ⊢ (𝐺 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
153	3, 152	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
154	153	simprd 478	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Cat)
155	1, 17, 46, 38, 84, 90, 110, 121, 99, 154	isfunc 16347	. . . 4 ⊢ (𝜑 → ((1st ‘(𝐺 ∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ ((1st ‘(𝐺 ∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ∧ (2nd ‘(𝐺 ∘func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐶)(((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func 𝐹))‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓))))))
156	29, 83, 151, 155	mpbir3and 1238	. . 3 ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)))
157		df-br 4584	. . 3 ⊢ ((1st ‘(𝐺 ∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
158	156, 157	sylib 207	. 2 ⊢ (𝜑 → ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
159	15, 158	eqeltrd 2688	1 ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ⟨cop 4131   class class class wbr 4583   × cxp 5036   ∘ ccom 5042  Rel wrel 5043   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1^st c1st 7057  2^nd c2nd 7058   ↑_𝑚 cmap 7744  Xcixp 7794  Basecbs 15695  Hom chom 15779  compcco 15780  Catccat 16148  Idccid 16149   Func cfunc 16337   ∘_func ccofu 16339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-ixp 7795  df-cat 16152  df-cid 16153  df-func 16341  df-cofu 16343

This theorem is referenced by:  cofuass  16372  cofull  16417  cofth  16418  catccatid  16575  1st2ndprf  16669  uncfcl  16698  uncf1  16699  uncf2  16700  yonedalem1  16735  yonedalem21  16736  yonedalem22  16741  funcrngcsetcALT  41791