Theorem cofucl 17921

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 2762	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
2		cofucl.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		cofucl.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))
4	1, 2, 3	cofuval 17915	. . 3 ⊢ (𝜑 → (𝐺 ∘func 𝐹) = ⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩)
5	1, 2, 3	cofu1st 17916	. . . 4 ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹)) = ((1st ‘𝐺) ∘ (1st ‘𝐹)))
6	4	fveq2d 6871	. . . . 5 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) = (2nd ‘⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩))
7		fvex 6880	. . . . . . 7 ⊢ (1st ‘𝐺) ∈ V
8		fvex 6880	. . . . . . 7 ⊢ (1st ‘𝐹) ∈ V
9	7, 8	coex 7911	. . . . . 6 ⊢ ((1st ‘𝐺) ∘ (1st ‘𝐹)) ∈ V
10		fvex 6880	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
11	10, 10	mpoex 8060	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) ∈ V
12	9, 11	op2nd 7979	. . . . 5 ⊢ (2nd ‘⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))
13	6, 12	eqtrdi 2813	. . . 4 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))))
14	5, 13	opeq12d 4839	. . 3 ⊢ (𝜑 → ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩ = ⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩)
15	4, 14	eqtr4d 2800	. 2 ⊢ (𝜑 → (𝐺 ∘func 𝐹) = ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩)
16		eqid 2762	. . . . . . 7 ⊢ (Base‘𝐷) = (Base‘𝐷)
17		eqid 2762	. . . . . . 7 ⊢ (Base‘𝐸) = (Base‘𝐸)
18		relfunc 17895	. . . . . . . 8 ⊢ Rel (𝐷 Func 𝐸)
19		1st2ndbr 8023	. . . . . . . 8 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝐺 ∈ (𝐷 Func 𝐸)) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
20	18, 3, 19	sylancr 596	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
21	16, 17, 20	funcf1 17899	. . . . . 6 ⊢ (𝜑 → (1st ‘𝐺):(Base‘𝐷)⟶(Base‘𝐸))
22		relfunc 17895	. . . . . . . 8 ⊢ Rel (𝐶 Func 𝐷)
23		1st2ndbr 8023	. . . . . . . 8 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
24	22, 2, 23	sylancr 596	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
25	1, 16, 24	funcf1 17899	. . . . . 6 ⊢ (𝜑 → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
26		fco 6716	. . . . . 6 ⊢ (((1st ‘𝐺):(Base‘𝐷)⟶(Base‘𝐸) ∧ (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) → ((1st ‘𝐺) ∘ (1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
27	21, 25, 26	syl2anc 593	. . . . 5 ⊢ (𝜑 → ((1st ‘𝐺) ∘ (1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
28	5	feq1d 6673	. . . . 5 ⊢ (𝜑 → ((1st ‘(𝐺 ∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ↔ ((1st ‘𝐺) ∘ (1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸)))
29	27, 28	mpbird 259	. . . 4 ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
30		eqid 2762	. . . . . . 7 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))
31		ovex 7429	. . . . . . . 8 ⊢ (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∈ V
32		ovex 7429	. . . . . . . 8 ⊢ (𝑥(2nd ‘𝐹)𝑦) ∈ V
33	31, 32	coex 7911	. . . . . . 7 ⊢ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ V
34	30, 33	fnmpoi 8051	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))
35	13	fneq1d 6614	. . . . . 6 ⊢ (𝜑 → ((2nd ‘(𝐺 ∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))))
36	34, 35	mpbiri 260	. . . . 5 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)))
37		eqid 2762	. . . . . . . . . . 11 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
38		eqid 2762	. . . . . . . . . . 11 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
39	20	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
40	25	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
41		simprl 780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
42	40, 41	ffvelcdmd 7066	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
43		simprr 782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
44	40, 43	ffvelcdmd 7066	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
45	16, 37, 38, 39, 42, 44	funcf2 17901	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
46		eqid 2762	. . . . . . . . . . 11 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
47	24	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
48	1, 46, 37, 47, 41, 43	funcf2 17901	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
49		fco 6716	. . . . . . . . . 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 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
51		ovex 7429	. . . . . . . . . 10 ⊢ (((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ∈ V
52		ovex 7429	. . . . . . . . . 10 ⊢ (𝑥(Hom ‘𝐶)𝑦) ∈ V
53	51, 52	elmap 8853	. . . . . . . . 9 ⊢ (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ ((((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦)) ↔ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
54	50, 53	sylibr 236	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ ((((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦)))
55	2	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
56	3	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸))
57	1, 55, 56, 41, 43	cofu2nd 17918	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))
58	1, 55, 56, 41	cofu1 17917	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑥) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)))
59	1, 55, 56, 43	cofu1 17917	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑦) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))
60	58, 59	oveq12d 7414	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) = (((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
61	60	oveq1d 7411	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)) = ((((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦)))
62	54, 57, 61	3eltr4d 2877	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
63	62	ralrimivva 3205	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
64		fveq2 6867	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) = ((2nd ‘(𝐺 ∘func 𝐹))‘⟨𝑥, 𝑦⟩))
65		df-ov 7399	. . . . . . . . 9 ⊢ (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) = ((2nd ‘(𝐺 ∘func 𝐹))‘⟨𝑥, 𝑦⟩)
66	64, 65	eqtr4di 2815	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) = (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦))
67		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
68		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
69	67, 68	op1std 7980	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑧) = 𝑥)
70	69	fveq2d 6871	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧)) = ((1st ‘(𝐺 ∘func 𝐹))‘𝑥))
71	67, 68	op2ndd 7981	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
72	71	fveq2d 6871	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧)) = ((1st ‘(𝐺 ∘func 𝐹))‘𝑦))
73	70, 72	oveq12d 7414	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) = (((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)))
74		fveq2 6867	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩))
75		df-ov 7399	. . . . . . . . . 10 ⊢ (𝑥(Hom ‘𝐶)𝑦) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩)
76	74, 75	eqtr4di 2815	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = (𝑥(Hom ‘𝐶)𝑦))
77	73, 76	oveq12d 7414	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) = ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
78	66, 77	eleq12d 2856	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦))))
79	78	ralxp 5813	. . . . . 6 ⊢ (∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
80	63, 79	sylibr 236	. . . . 5 ⊢ (𝜑 → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
81		fvex 6880	. . . . . 6 ⊢ (2nd ‘(𝐺 ∘func 𝐹)) ∈ V
82	81	elixp 8886	. . . . 5 ⊢ ((2nd ‘(𝐺 ∘func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ ((2nd ‘(𝐺 ∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧))))
83	36, 80, 82	sylanbrc 592	. . . 4 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
84		eqid 2762	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
85		eqid 2762	. . . . . . . . . 10 ⊢ (Id‘𝐷) = (Id‘𝐷)
86	24	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
87		simpr 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
88	1, 84, 85, 86, 87	funcid 17903	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)))
89	88	fveq2d 6871	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))))
90		eqid 2762	. . . . . . . . 9 ⊢ (Id‘𝐸) = (Id‘𝐸)
91	20	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
92	25	ffvelcdmda 7065	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
93	16, 85, 90, 91, 92	funcid 17903	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))))
94	89, 93	eqtrd 2797	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))))
95	2	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
96	3	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐷 Func 𝐸))
97		funcrcl 17896	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
98	2, 97	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
99	98	simpld 498	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ Cat)
100	99	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
101	1, 46, 84, 100, 87	catidcl 17714	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
102	1, 95, 96, 87, 87, 46, 101	cofu2 17919	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))))
103	1, 95, 96, 87	cofu1 17917	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑥) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)))
104	103	fveq2d 6871	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸)‘((1st ‘(𝐺 ∘func 𝐹))‘𝑥)) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))))
105	94, 102, 104	3eqtr4d 2807	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func 𝐹))‘𝑥)))
106	86	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
107		simplr 778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ (Base‘𝐶))
108		simprlr 789	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ (Base‘𝐶))
109	1, 46, 37, 106, 107, 108	funcf2 17901	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
110		eqid 2762	. . . . . . . . . . . . 13 ⊢ (comp‘𝐶) = (comp‘𝐶)
111	100	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐶 ∈ Cat)
112		simprll 788	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ (Base‘𝐶))
113		simprrl 790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
114		simprrr 791	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
115	1, 46, 110, 111, 107, 112, 108, 113, 114	catcocl 17717	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
116		fvco3 6967	. . . . . . . . . . . 12 ⊢ (((𝑥(2nd ‘𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
117	109, 115, 116	syl2anc 593	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
118		eqid 2762	. . . . . . . . . . . . 13 ⊢ (comp‘𝐷) = (comp‘𝐷)
119	1, 46, 110, 118, 106, 107, 112, 108, 113, 114	funcco 17904	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))
120	119	fveq2d 6871	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓))))
121		eqid 2762	. . . . . . . . . . . 12 ⊢ (comp‘𝐸) = (comp‘𝐸)
122	91	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
123	92	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
124	25	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
125	124	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
126	125, 112	ffvelcdmd 7066	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
127	125, 108	ffvelcdmd 7066	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷))
128	1, 46, 37, 106, 107, 112	funcf2 17901	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
129	128, 113	ffvelcdmd 7066	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘𝐹)𝑦)‘𝑓) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
130	1, 46, 37, 106, 112, 108	funcf2 17901	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
131	130, 114	ffvelcdmd 7066	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
132	16, 37, 118, 121, 122, 123, 126, 127, 129, 131	funcco 17904	. . . . . . . . . . 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 2801	. . . . . . . . . 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 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐹 ∈ (𝐶 Func 𝐷))
135	96	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐺 ∈ (𝐷 Func 𝐸))
136	1, 134, 135, 107, 108	cofu2nd 17918	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧)))
137	136	fveq1d 6869	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
138	103	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑥) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)))
139	1, 134, 135, 112	cofu1 17917	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑦) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))
140	138, 139	opeq12d 4839	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩ = ⟨((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))⟩)
141	1, 134, 135, 108	cofu1 17917	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑧) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))
142	140, 141	oveq12d 7414	. . . . . . . . . . 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 17919	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔) = ((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔)))
144	1, 134, 135, 107, 112, 46, 113	cofu2 17919	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))
145	142, 143, 144	oveq123d 7417	. . . . . . . . . 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 2807	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
147	146	anassrs 471	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
148	147	ralrimivva 3205	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
149	148	ralrimivva 3205	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
150	105, 149	jca 519	. . . . 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 3154	. . . 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 17896	. . . . . . 7 ⊢ (𝐺 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
153	3, 152	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
154	153	simprd 499	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Cat)
155	1, 17, 46, 38, 84, 90, 110, 121, 99, 154	isfunc 17897	. . . 4 ⊢ (𝜑 → ((1st ‘(𝐺 ∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ ((1st ‘(𝐺 ∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ∧ (2nd ‘(𝐺 ∘func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((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 1356	. . 3 ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)))
157		df-br 5101	. . 3 ⊢ ((1st ‘(𝐺 ∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
158	156, 157	sylib 220	. 2 ⊢ (𝜑 → ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
159	15, 158	eqeltrd 2862	1 ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∀wral 3076  ⟨cop 4588   class class class wbr 5100   × cxp 5645   ∘ ccom 5651  Rel wrel 5652   Fn wfn 6516  ⟶wf 6517  ‘cfv 6521  (class class class)co 7396   ∈ cmpo 7398  1^st c1st 7968  2^nd c2nd 7969   ↑_m cmap 8808  Xcixp 8879  Basecbs 17245  Hom chom 17297  compcco 17298  Catccat 17696  Idccid 17697   Func cfunc 17887   ∘_func ccofu 17889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-map 8810  df-ixp 8880  df-cat 17700  df-cid 17701  df-func 17891  df-cofu 17893

This theorem is referenced by:  cofuass  17922  cofull  17969  cofth  17970  catccatid  18139  1st2ndprf  18238  uncfcl  18267  uncf1  18268  uncf2  18269  yonedalem1  18304  yonedalem21  18305  yonedalem22  18310  funcrngcsetcALT  20691  rescofuf  49714  cofu1a  49715  cofu2a  49716  cofucla  49717  cofuoppf  49771  uptrlem2  49832  uptra  49836  uptr2a  49843  cofuswapfcl  49914  prcofdiag1  50014  prcofdiag  50015  oppfdiag1  50035  oppfdiag  50037  cofuterm  50166