Theorem cofucl 17774

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 2736	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
2		cofucl.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		cofucl.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸))
4	1, 2, 3	cofuval 17768	. . 3 ⊢ (𝜑 → (𝐺 ∘func 𝐹) = ⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩)
5	1, 2, 3	cofu1st 17769	. . . 4 ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹)) = ((1st ‘𝐺) ∘ (1st ‘𝐹)))
6	4	fveq2d 6846	. . . . 5 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) = (2nd ‘⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩))
7		fvex 6855	. . . . . . 7 ⊢ (1st ‘𝐺) ∈ V
8		fvex 6855	. . . . . . 7 ⊢ (1st ‘𝐹) ∈ V
9	7, 8	coex 7867	. . . . . 6 ⊢ ((1st ‘𝐺) ∘ (1st ‘𝐹)) ∈ V
10		fvex 6855	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
11	10, 10	mpoex 8012	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) ∈ V
12	9, 11	op2nd 7930	. . . . 5 ⊢ (2nd ‘⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))
13	6, 12	eqtrdi 2792	. . . 4 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))))
14	5, 13	opeq12d 4838	. . 3 ⊢ (𝜑 → ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩ = ⟨((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))⟩)
15	4, 14	eqtr4d 2779	. 2 ⊢ (𝜑 → (𝐺 ∘func 𝐹) = ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩)
16		eqid 2736	. . . . . . 7 ⊢ (Base‘𝐷) = (Base‘𝐷)
17		eqid 2736	. . . . . . 7 ⊢ (Base‘𝐸) = (Base‘𝐸)
18		relfunc 17748	. . . . . . . 8 ⊢ Rel (𝐷 Func 𝐸)
19		1st2ndbr 7974	. . . . . . . 8 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝐺 ∈ (𝐷 Func 𝐸)) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
20	18, 3, 19	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
21	16, 17, 20	funcf1 17752	. . . . . 6 ⊢ (𝜑 → (1st ‘𝐺):(Base‘𝐷)⟶(Base‘𝐸))
22		relfunc 17748	. . . . . . . 8 ⊢ Rel (𝐶 Func 𝐷)
23		1st2ndbr 7974	. . . . . . . 8 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
24	22, 2, 23	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
25	1, 16, 24	funcf1 17752	. . . . . 6 ⊢ (𝜑 → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
26		fco 6692	. . . . . 6 ⊢ (((1st ‘𝐺):(Base‘𝐷)⟶(Base‘𝐸) ∧ (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) → ((1st ‘𝐺) ∘ (1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
27	21, 25, 26	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((1st ‘𝐺) ∘ (1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
28	5	feq1d 6653	. . . . 5 ⊢ (𝜑 → ((1st ‘(𝐺 ∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ↔ ((1st ‘𝐺) ∘ (1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸)))
29	27, 28	mpbird 256	. . . 4 ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸))
30		eqid 2736	. . . . . . 7 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))
31		ovex 7390	. . . . . . . 8 ⊢ (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∈ V
32		ovex 7390	. . . . . . . 8 ⊢ (𝑥(2nd ‘𝐹)𝑦) ∈ V
33	31, 32	coex 7867	. . . . . . 7 ⊢ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ V
34	30, 33	fnmpoi 8002	. . . . . 6 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))
35	13	fneq1d 6595	. . . . . 6 ⊢ (𝜑 → ((2nd ‘(𝐺 ∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶))))
36	34, 35	mpbiri 257	. . . . 5 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)))
37		eqid 2736	. . . . . . . . . . 11 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
38		eqid 2736	. . . . . . . . . . 11 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
39	20	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
40	25	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
41		simprl 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
42	40, 41	ffvelcdmd 7036	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
43		simprr 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
44	40, 43	ffvelcdmd 7036	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
45	16, 37, 38, 39, 42, 44	funcf2 17754	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
46		eqid 2736	. . . . . . . . . . 11 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
47	24	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
48	1, 46, 37, 47, 41, 43	funcf2 17754	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
49		fco 6692	. . . . . . . . . 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 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
51		ovex 7390	. . . . . . . . . 10 ⊢ (((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ∈ V
52		ovex 7390	. . . . . . . . . 10 ⊢ (𝑥(Hom ‘𝐶)𝑦) ∈ V
53	51, 52	elmap 8809	. . . . . . . . 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 233	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ ((((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦)))
55	2	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
56	3	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸))
57	1, 55, 56, 41, 43	cofu2nd 17771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))
58	1, 55, 56, 41	cofu1 17770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑥) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)))
59	1, 55, 56, 43	cofu1 17770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑦) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))
60	58, 59	oveq12d 7375	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) = (((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))
61	60	oveq1d 7372	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)) = ((((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦)))
62	54, 57, 61	3eltr4d 2853	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
63	62	ralrimivva 3197	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
64		fveq2 6842	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) = ((2nd ‘(𝐺 ∘func 𝐹))‘⟨𝑥, 𝑦⟩))
65		df-ov 7360	. . . . . . . . 9 ⊢ (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) = ((2nd ‘(𝐺 ∘func 𝐹))‘⟨𝑥, 𝑦⟩)
66	64, 65	eqtr4di 2794	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) = (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦))
67		vex 3449	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
68		vex 3449	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
69	67, 68	op1std 7931	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑧) = 𝑥)
70	69	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧)) = ((1st ‘(𝐺 ∘func 𝐹))‘𝑥))
71	67, 68	op2ndd 7932	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
72	71	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧)) = ((1st ‘(𝐺 ∘func 𝐹))‘𝑦))
73	70, 72	oveq12d 7375	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) = (((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)))
74		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩))
75		df-ov 7360	. . . . . . . . . 10 ⊢ (𝑥(Hom ‘𝐶)𝑦) = ((Hom ‘𝐶)‘⟨𝑥, 𝑦⟩)
76	74, 75	eqtr4di 2794	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐶)‘𝑧) = (𝑥(Hom ‘𝐶)𝑦))
77	73, 76	oveq12d 7375	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) = ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))
78	66, 77	eleq12d 2832	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)) ↔ (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦))))
79	78	ralxp 5797	. . . . . 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 233	. . . . 5 ⊢ (𝜑 → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
81		fvex 6855	. . . . . 6 ⊢ (2nd ‘(𝐺 ∘func 𝐹)) ∈ V
82	81	elixp 8842	. . . . 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 583	. . . 4 ⊢ (𝜑 → (2nd ‘(𝐺 ∘func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st ‘(𝐺 ∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐶)‘𝑧)))
84		eqid 2736	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
85		eqid 2736	. . . . . . . . . 10 ⊢ (Id‘𝐷) = (Id‘𝐷)
86	24	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
87		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
88	1, 84, 85, 86, 87	funcid 17756	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)))
89	88	fveq2d 6846	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))))
90		eqid 2736	. . . . . . . . 9 ⊢ (Id‘𝐸) = (Id‘𝐸)
91	20	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
92	25	ffvelcdmda 7035	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
93	16, 85, 90, 91, 92	funcid 17756	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))))
94	89, 93	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))))
95	2	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
96	3	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐷 Func 𝐸))
97		funcrcl 17749	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
98	2, 97	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
99	98	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ Cat)
100	99	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
101	1, 46, 84, 100, 87	catidcl 17562	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
102	1, 95, 96, 87, 87, 46, 101	cofu2 17772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))))
103	1, 95, 96, 87	cofu1 17770	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑥) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)))
104	103	fveq2d 6846	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸)‘((1st ‘(𝐺 ∘func 𝐹))‘𝑥)) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))))
105	94, 102, 104	3eqtr4d 2786	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func 𝐹))‘𝑥)))
106	86	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
107		simplr 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ (Base‘𝐶))
108		simprlr 778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ (Base‘𝐶))
109	1, 46, 37, 106, 107, 108	funcf2 17754	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
110		eqid 2736	. . . . . . . . . . . . 13 ⊢ (comp‘𝐶) = (comp‘𝐶)
111	100	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐶 ∈ Cat)
112		simprll 777	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ (Base‘𝐶))
113		simprrl 779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
114		simprrr 780	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
115	1, 46, 110, 111, 107, 112, 108, 113, 114	catcocl 17565	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
116		fvco3 6940	. . . . . . . . . . . 12 ⊢ (((𝑥(2nd ‘𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
117	109, 115, 116	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
118		eqid 2736	. . . . . . . . . . . . 13 ⊢ (comp‘𝐷) = (comp‘𝐷)
119	1, 46, 110, 118, 106, 107, 112, 108, 113, 114	funcco 17757	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))
120	119	fveq2d 6846	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓))))
121		eqid 2736	. . . . . . . . . . . 12 ⊢ (comp‘𝐸) = (comp‘𝐸)
122	91	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺))
123	92	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
124	25	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
125	124	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷))
126	125, 112	ffvelcdmd 7036	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
127	125, 108	ffvelcdmd 7036	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷))
128	1, 46, 37, 106, 107, 112	funcf2 17754	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
129	128, 113	ffvelcdmd 7036	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘𝐹)𝑦)‘𝑓) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)))
130	1, 46, 37, 106, 112, 108	funcf2 17754	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
131	130, 114	ffvelcdmd 7036	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)))
132	16, 37, 118, 121, 122, 123, 126, 127, 129, 131	funcco 17757	. . . . . . . . . . 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 2780	. . . . . . . . . 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 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐹 ∈ (𝐶 Func 𝐷))
135	96	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐺 ∈ (𝐷 Func 𝐸))
136	1, 134, 135, 107, 108	cofu2nd 17771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧)))
137	136	fveq1d 6844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
138	103	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑥) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)))
139	1, 134, 135, 112	cofu1 17770	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑦) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))
140	138, 139	opeq12d 4838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩ = ⟨((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥)), ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))⟩)
141	1, 134, 135, 108	cofu1 17770	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func 𝐹))‘𝑧) = ((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))
142	140, 141	oveq12d 7375	. . . . . . . . . . 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 17772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔) = ((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔)))
144	1, 134, 135, 107, 112, 46, 113	cofu2 17772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))
145	142, 143, 144	oveq123d 7378	. . . . . . . . . 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 2786	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
147	146	anassrs 468	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
148	147	ralrimivva 3197	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
149	148	ralrimivva 3197	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(⟨((1st ‘(𝐺 ∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)⟩(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))
150	105, 149	jca 512	. . . . 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 3143	. . . 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 17749	. . . . . . 7 ⊢ (𝐺 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
153	3, 152	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
154	153	simprd 496	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Cat)
155	1, 17, 46, 38, 84, 90, 110, 121, 99, 154	isfunc 17750	. . . 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 1342	. . 3 ⊢ (𝜑 → (1st ‘(𝐺 ∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)))
157		df-br 5106	. . 3 ⊢ ((1st ‘(𝐺 ∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
158	156, 157	sylib 217	. 2 ⊢ (𝜑 → ⟨(1st ‘(𝐺 ∘func 𝐹)), (2nd ‘(𝐺 ∘func 𝐹))⟩ ∈ (𝐶 Func 𝐸))
159	15, 158	eqeltrd 2838	1 ⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3064  ⟨cop 4592   class class class wbr 5105   × cxp 5631   ∘ ccom 5637  Rel wrel 5638   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357   ∈ cmpo 7359  1^st c1st 7919  2^nd c2nd 7920   ↑_m cmap 8765  Xcixp 8835  Basecbs 17083  Hom chom 17144  compcco 17145  Catccat 17544  Idccid 17545   Func cfunc 17740   ∘_func ccofu 17742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767  df-ixp 8836  df-cat 17548  df-cid 17549  df-func 17744  df-cofu 17746

This theorem is referenced by:  cofuass  17775  cofull  17821  cofth  17822  catccatid  17992  1st2ndprf  18094  uncfcl  18124  uncf1  18125  uncf2  18126  yonedalem1  18161  yonedalem21  18162  yonedalem22  18167  funcrngcsetcALT  46287