curfcl

Description: The curry functor of a functor F : C X. D --> E is a functor curryF ( F ) : C --> ( D --> E ) . (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	curfcl.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
	curfcl.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐸 )
	curfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	curfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	curfcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
Assertion	curfcl	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		curfcl.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
2		curfcl.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐸 )
3		curfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		curfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		curfcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
10		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
11		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
12	1 6 3 4 5 7 8 9 10 11	curfval	⊢ ( 𝜑 → 𝐺 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
13		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
14	13	mptex	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) ∈ V
15	13 13	mpoex	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ∈ V
16	14 15	op1std	⊢ ( 𝐺 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ → ( 1^st ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )
17	12 16	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )
18	14 15	op2ndd	⊢ ( 𝐺 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ → ( 2^nd ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) )
19	12 18	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) )
20	17 19	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
21	12 20	eqtr4d	⊢ ( 𝜑 → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
22	2	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ 𝑄 )
23		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
24	2 23	fuchom	⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ 𝑄 )
25		eqid	⊢ ( Id ‘ 𝑄 ) = ( Id ‘ 𝑄 )
26		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
27		eqid	⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 )
28		funcrcl	⊢ ( 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) → ( ( 𝐶 ×_c 𝐷 ) ∈ Cat ∧ 𝐸 ∈ Cat ) )
29	5 28	syl	⊢ ( 𝜑 → ( ( 𝐶 ×_c 𝐷 ) ∈ Cat ∧ 𝐸 ∈ Cat ) )
30	29	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
31	2 4 30	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
32		opex	⊢ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ∈ V
33	32	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ∈ V )
34	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
35	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
36	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
38		eqid	⊢ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 )
39	1 6 34 35 36 7 37 38	curf1cl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) )
40	33 17 39	fmpt2d	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( 𝐷 Func 𝐸 ) )
41		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
42		ovex	⊢ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∈ V
43	42	mptex	⊢ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ∈ V
44	41 43	fnmpoi	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
45	19	fneq1d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝐺 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
46	44 45	mpbiri	⊢ ( 𝜑 → ( 2^nd ‘ 𝐺 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
47		fvex	⊢ ( Base ‘ 𝐷 ) ∈ V
48	47	mptex	⊢ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ∈ V
49	48	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ∈ V )
50	19	oveqd	⊢ ( 𝜑 → ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) 𝑦 ) )
51	41	ovmpt4g	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ∈ V ) → ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) 𝑦 ) = ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
52	43 51	mp3an3	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) 𝑦 ) = ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
53	50 52	sylan9eq	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) = ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
54	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐶 ∈ Cat )
55	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐷 ∈ Cat )
56	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
57		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
58		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
59		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
60		eqid	⊢ ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) = ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 )
61	1 6 54 55 56 7 10 11 57 58 59 60 23	curf2cl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
62	49 53 61	fmpt2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
63		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
64	63 6 7	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ ( 𝐶 ×_c 𝐷 ) )
65		eqid	⊢ ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Id ‘ ( 𝐶 ×_c 𝐷 ) )
66		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
67		relfunc	⊢ Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 )
68		1st2ndbr	⊢ ( ( Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ∧ 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
69	67 5 68	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
70	69	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
71		opelxpi	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
72	71	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
73	64 65 66 70 72	funcid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ( ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
74	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐶 ∈ Cat )
75	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐷 ∈ Cat )
76	37	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
77		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
78	63 74 75 6 7 9 11 65 76 77	xpcid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ⟩ )
79	78	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ( ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ⟩ ) )
80		df-ov	⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ⟩ )
81	79 80	eqtr4di	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ( ( Id ‘ ( 𝐶 ×_c 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) )
82	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
83	1 6 74 75 82 7 76 38 77	curf11	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) )
84		df-ov	⊢ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
85	83 84	eqtr2di	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) )
86	85	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) )
87	73 81 86	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) )
88	87	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) ) )
89	30	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
90		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
91	90 66	cidfn	⊢ ( 𝐸 ∈ Cat → ( Id ‘ 𝐸 ) Fn ( Base ‘ 𝐸 ) )
92	89 91	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( Id ‘ 𝐸 ) Fn ( Base ‘ 𝐸 ) )
93		dffn2	⊢ ( ( Id ‘ 𝐸 ) Fn ( Base ‘ 𝐸 ) ↔ ( Id ‘ 𝐸 ) : ( Base ‘ 𝐸 ) ⟶ V )
94	92 93	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( Id ‘ 𝐸 ) : ( Base ‘ 𝐸 ) ⟶ V )
95		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
96		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
97	95 39 96	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
98	7 90 97	funcf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
99		fcompt	⊢ ( ( ( Id ‘ 𝐸 ) : ( Base ‘ 𝐸 ) ⟶ V ∧ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) ) → ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) ) )
100	94 98 99	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) ) )
101	88 100	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) ) = ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
102	6 10 9 34 37	catidcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
103		eqid	⊢ ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
104	1 6 34 35 36 7 10 11 37 37 102 103	curf2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) ) )
105	2 25 66 39	fucid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑄 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
106	101 104 105	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑄 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
107	3	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
108	107	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝐶 ∈ Cat )
109	4	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐷 ∈ Cat )
110	109	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝐷 ∈ Cat )
111	5	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
112	111	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
113		simp21	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
114	113	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
115		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑤 ∈ ( Base ‘ 𝐷 ) )
116	1 6 108 110 112 7 114 38 115	curf11	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑤 ) )
117		df-ov	⊢ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ )
118	116 117	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) )
119		simp22	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
120	119	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
121		eqid	⊢ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 )
122	1 6 108 110 112 7 120 121 115	curf11	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) = ( 𝑦 ( 1^st ‘ 𝐹 ) 𝑤 ) )
123		df-ov	⊢ ( 𝑦 ( 1^st ‘ 𝐹 ) 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ )
124	122 123	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) )
125	118 124	opeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) ⟩ )
126		simp23	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
127	126	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
128		eqid	⊢ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 )
129	1 6 108 110 112 7 127 128 115	curf11	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) = ( 𝑧 ( 1^st ‘ 𝐹 ) 𝑤 ) )
130		df-ov	⊢ ( 𝑧 ( 1^st ‘ 𝐹 ) 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ )
131	129 130	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
132	125 131	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
133		simp3r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
134	133	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
135		eqid	⊢ ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) = ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 )
136	1 6 108 110 112 7 10 11 120 127 134 135 115	curf2val	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) )
137		df-ov	⊢ ( 𝑔 ( ⟨ 𝑦 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ⟨ 𝑦 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
138	136 137	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) = ( ( ⟨ 𝑦 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) )
139		simp3l	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
140	139	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
141		eqid	⊢ ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 )
142	1 6 108 110 112 7 10 11 114 120 140 141 115	curf2val	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) )
143		df-ov	⊢ ( 𝑓 ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
144	142 143	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) )
145	132 138 144	oveq123d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) ) = ( ( ( ⟨ 𝑦 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ) )
146		eqid	⊢ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×_c 𝐷 ) )
147		eqid	⊢ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) = ( comp ‘ ( 𝐶 ×_c 𝐷 ) )
148		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
149	67 112 68	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
150		opelxpi	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
151	113 150	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
152		opelxpi	⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑦 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
153	119 152	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑦 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
154		opelxpi	⊢ ( ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
155	126 154	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
156	7 8 11 110 115	catidcl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ∈ ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) )
157	140 156	opelxpd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ∈ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
158	63 6 7 10 8 114 115 120 115 146	xpchom2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ 𝑥 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑤 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
159	157 158	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ∈ ( ⟨ 𝑥 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑤 ⟩ ) )
160	134 156	opelxpd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ∈ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
161	63 6 7 10 8 120 115 127 115 146	xpchom2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ 𝑦 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
162	160 161	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ∈ ( ⟨ 𝑦 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) )
163	64 146 147 148 149 151 153 155 159 162	funcco	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑤 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ) = ( ( ( ⟨ 𝑦 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ) )
164		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
165	63 6 7 10 8 114 115 120 115 26 164 147 127 115 140 156 134 156	xpcco2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑤 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) = ⟨ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) , ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑤 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) ⟩ )
166	7 8 11 110 115 164 115 156	catlid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑤 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) )
167	166	opeq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) , ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑤 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) ⟩ = ⟨ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
168	165 167	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑤 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) = ⟨ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
169	168	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑤 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) )
170		df-ov	⊢ ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
171	169 170	eqtr4di	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑤 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ) = ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) )
172	145 163 171	3eqtr2rd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) ) )
173	172	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) ) ) )
174	6 10 26 107 113 119 126 139 133	catcocl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
175		eqid	⊢ ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
176	1 6 107 109 111 7 10 11 113 126 174 175	curf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) ) )
177	1 6 107 109 111 7 10 11 113 119 139 141 23	curf2cl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
178	1 6 107 109 111 7 10 11 119 126 133 135 23	curf2cl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) )
179	2 23 7 148 27 177 178	fucco	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑄 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) = ( 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) ) ) )
180	173 176 179	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑄 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) )
181	6 22 10 24 9 25 26 27 3 31 40 46 62 106 180	isfuncd	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝐺 ) )
182		df-br	⊢ ( ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝐺 ) ↔ ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ∈ ( 𝐶 Func 𝑄 ) )
183	181 182	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ∈ ( 𝐶 Func 𝑄 ) )
184	21 183	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝑄 ) )

Metamath Proof Explorer

Theorem curfcl

Proof