curfuncf

Description: Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	uncfval.g	⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 )
	uncfval.c	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	uncfval.d	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	uncfval.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
Assertion	curfuncf	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 ) = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		uncfval.g	⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 )
2		uncfval.c	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		uncfval.d	⊢ ( 𝜑 → 𝐸 ∈ Cat )
4		uncfval.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
5	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐷 ∈ Cat )
6	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐸 ∈ Cat )
7	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
11		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
12	1 5 6 7 8 9 10 11	uncf1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) )
13	12	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) )
14		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
15		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
16		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
17	16	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
18		relfunc	⊢ Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) )
19		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ∧ 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2^nd ‘ 𝐺 ) )
20	18 4 19	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2^nd ‘ 𝐺 ) )
21	8 17 20	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( 𝐷 Func 𝐸 ) )
22	21	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) )
23		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
24	15 22 23	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
25	9 14 24	funcf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
26	25	feqmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) )
27	13 26	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) = ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
28	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐷 ∈ Cat )
29	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐸 ∈ Cat )
30	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
31		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
32		simplrl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
33		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
34		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
35		simprr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
36	35	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
37		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
38		funcrcl	⊢ ( 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
39	4 38	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
40	39	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
41	40	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐶 ∈ Cat )
42	8 33 37 41 31	catidcl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
43		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
44	1 28 29 30 8 9 31 32 33 34 31 36 42 43	uncf2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) = ( ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ 𝑔 ) ) )
45		eqid	⊢ ( Id ‘ ( 𝐷 FuncCat 𝐸 ) ) = ( Id ‘ ( 𝐷 FuncCat 𝐸 ) )
46	20	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2^nd ‘ 𝐺 ) )
47	8 37 45 46 31	funcid	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ ( 𝐷 FuncCat 𝐸 ) ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
48		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
49	22	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) )
50	16 45 48 49	fucid	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( Id ‘ ( 𝐷 FuncCat 𝐸 ) ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
51	47 50	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
52	51	fveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ‘ 𝑧 ) = ( ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ‘ 𝑧 ) )
53	25	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
54		fvco3	⊢ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) )
55	53 36 54	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( Id ‘ 𝐸 ) ∘ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) )
56	52 55	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ‘ 𝑧 ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) )
57	56	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ 𝑔 ) ) = ( ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ 𝑔 ) ) )
58		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
59	53 32	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐸 ) )
60		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
61	53 36	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐸 ) )
62	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
63		simprl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
64	9 34 58 62 63 35	funcf2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) )
65	64	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) )
66	14 58 48 29 59 60 61 65	catlid	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ 𝑔 ) ) = ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ 𝑔 ) )
67	44 57 66	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) = ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ 𝑔 ) )
68	67	mpteq2dva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ 𝑔 ) ) )
69	64	feqmptd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) = ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ 𝑔 ) ) )
70	68 69	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) = ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) )
71	70	3impb	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) = ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) )
72	71	mpoeq3dva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ) )
73	9 24	funcfn2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
74		fnov	⊢ ( ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↔ ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ) )
75	73 74	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ) )
76	72 75	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) = ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
77	27 76	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ )
78		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ )
79	15 22 78	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ )
80	77 79	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ = ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) )
81	80	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
82	21	feqmptd	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
83	81 82	eqtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) = ( 1^st ‘ 𝐺 ) )
84	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝐷 ∈ Cat )
85	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝐸 ∈ Cat )
86	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
87		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
88	87	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
89		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
90		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
91	90	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
92		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
93		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
94	9 34 93 84 89	catidcl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) )
95	1 84 85 86 8 9 88 89 33 34 91 89 92 94	uncf2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑧 ) ) ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) )
96	22	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) )
97	96	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) )
98	15 97 23	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
99	98	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
100	9 93 48 99 89	funcid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) )
101	100	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑧 ) ) ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑧 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) = ( ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑧 ) ) ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) ) )
102	9 14 98	funcf1	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
103	102	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐸 ) )
104	21	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝐷 Func 𝐸 ) )
105	104	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝐷 Func 𝐸 ) )
106	105	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝐷 Func 𝐸 ) )
107		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
108	15 106 107	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
109	9 14 108	funcf1	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
110	109	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐸 ) )
111		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
112	16 111	fuchom	⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ ( 𝐷 FuncCat 𝐸 ) )
113	20	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2^nd ‘ 𝐺 ) )
114	8 33 112 113 88 91	funcf2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
115	114 92	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
116	111 115	nat1st2nd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ∈ ( ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ⟩ ) )
117	111 116 9 58 89	natcl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑧 ) ) )
118	14 58 48 85 103 60 110 117	catrid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑧 ) ) ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑧 ) ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) )
119	95 101 118	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) )
120	119	mpteq2dva	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) ) )
121	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2^nd ‘ 𝐺 ) )
122	8 33 112 121 87 90	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
123	122	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
124	111 123	nat1st2nd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ∈ ( ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ⟩ ) )
125	111 124 9	natfn	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) Fn ( Base ‘ 𝐷 ) )
126		dffn5	⊢ ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) Fn ( Base ‘ 𝐷 ) ↔ ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) ) )
127	125 126	sylib	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑧 ) ) )
128	120 127	eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) )
129	128	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) = ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ) )
130	122	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) = ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ) )
131	129 130	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) = ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) )
132	131	3impb	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) = ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) )
133	132	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) )
134	8 20	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ 𝐺 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
135		fnov	⊢ ( ( 2^nd ‘ 𝐺 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 2^nd ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) )
136	134 135	sylib	⊢ ( 𝜑 → ( 2^nd ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) )
137	133 136	eqtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) = ( 2^nd ‘ 𝐺 ) )
138	83 137	opeq12d	⊢ ( 𝜑 → ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
139		eqid	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 ) = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
140	1 2 3 4	uncfcl	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
141	139 8 40 2 140 9 34 37 33 93	curfval	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 ) = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
142		1st2nd	⊢ ( ( Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ∧ 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ) → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
143	18 4 142	sylancr	⊢ ( 𝜑 → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
144	138 141 143	3eqtr4d	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 ) = 𝐺 )

Metamath Proof Explorer

Theorem curfuncf

Proof