evlfcl

Description: The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors C --> D , and the second parameter in D . (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	evlfcl.e	⊢ 𝐸 = ( 𝐶 eval_F 𝐷 )
	evlfcl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	evlfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	evlfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	evlfcl	⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑄 ×_c 𝐶 ) Func 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		evlfcl.e	⊢ 𝐸 = ( 𝐶 eval_F 𝐷 )
2		evlfcl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
3		evlfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		evlfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
8		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
9	1 3 4 5 6 7 8	evlfval	⊢ ( 𝜑 → 𝐸 = ⟨ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩ )
10		ovex	⊢ ( 𝐶 Func 𝐷 ) ∈ V
11		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
12	10 11	mpoex	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ∈ V
13	10 11	xpex	⊢ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∈ V
14	13 13	mpoex	⊢ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ∈ V
15	12 14	opelvv	⊢ ⟨ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩ ∈ ( V × V )
16	9 15	eqeltrdi	⊢ ( 𝜑 → 𝐸 ∈ ( V × V ) )
17		1st2nd2	⊢ ( 𝐸 ∈ ( V × V ) → 𝐸 = ⟨ ( 1^st ‘ 𝐸 ) , ( 2^nd ‘ 𝐸 ) ⟩ )
18	16 17	syl	⊢ ( 𝜑 → 𝐸 = ⟨ ( 1^st ‘ 𝐸 ) , ( 2^nd ‘ 𝐸 ) ⟩ )
19		eqid	⊢ ( 𝑄 ×_c 𝐶 ) = ( 𝑄 ×_c 𝐶 )
20	2	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
21	19 20 5	xpcbas	⊢ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) = ( Base ‘ ( 𝑄 ×_c 𝐶 ) )
22		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
23		eqid	⊢ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) = ( Hom ‘ ( 𝑄 ×_c 𝐶 ) )
24		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
25		eqid	⊢ ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) = ( Id ‘ ( 𝑄 ×_c 𝐶 ) )
26		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
27		eqid	⊢ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) = ( comp ‘ ( 𝑄 ×_c 𝐶 ) )
28	2 3 4	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
29	19 28 3	xpccat	⊢ ( 𝜑 → ( 𝑄 ×_c 𝐶 ) ∈ Cat )
30		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
32		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑓 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑓 ) )
33	30 31 32	sylancr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑓 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑓 ) )
34	5 22 33	funcf1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
35	34	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
36	35	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
37	36	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
38		eqid	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) )
39	38	fmpo	⊢ ( ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) ↔ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) : ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ⟶ ( Base ‘ 𝐷 ) )
40	37 39	sylib	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) : ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ⟶ ( Base ‘ 𝐷 ) )
41	12 14	op1std	⊢ ( 𝐸 = ⟨ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩ → ( 1^st ‘ 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) )
42	9 41	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) )
43	42	feq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐸 ) : ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ⟶ ( Base ‘ 𝐷 ) ↔ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) : ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ⟶ ( Base ‘ 𝐷 ) ) )
44	40 43	mpbird	⊢ ( 𝜑 → ( 1^st ‘ 𝐸 ) : ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ⟶ ( Base ‘ 𝐷 ) )
45		eqid	⊢ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) = ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) )
46		ovex	⊢ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) ∈ V
47		ovex	⊢ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ∈ V
48	46 47	mpoex	⊢ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ∈ V
49	48	csbex	⊢ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ∈ V
50	49	csbex	⊢ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ∈ V
51	45 50	fnmpoi	⊢ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) Fn ( ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) × ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) )
52	12 14	op2ndd	⊢ ( 𝐸 = ⟨ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩ → ( 2^nd ‘ 𝐸 ) = ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) )
53	9 52	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝐸 ) = ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) )
54	53	fneq1d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝐸 ) Fn ( ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) × ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ↔ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) Fn ( ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) × ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ) )
55	51 54	mpbiri	⊢ ( 𝜑 → ( 2^nd ‘ 𝐸 ) Fn ( ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) × ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) )
56	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐷 ∈ Cat )
57	56	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → 𝐷 ∈ Cat )
58		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
59	30 58 32	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑓 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑓 ) )
60	5 22 59	funcf1	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
61	60	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ( 1^st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
62		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
63	62	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
64	61 63	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ∈ ( Base ‘ 𝐷 ) )
65		simplrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → 𝑣 ∈ ( Base ‘ 𝐶 ) )
66	61 65	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ∈ ( Base ‘ 𝐷 ) )
67		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑔 ∈ ( 𝐶 Func 𝐷 ) )
68		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑔 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑔 ) )
69	30 67 68	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑔 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑔 ) )
70	5 22 69	funcf1	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑔 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
71	70	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ( 1^st ‘ 𝑔 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
72	71 65	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ∈ ( Base ‘ 𝐷 ) )
73		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑣 ∈ ( Base ‘ 𝐶 ) )
74	5 6 24 59 62 73	funcf2	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) : ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ⟶ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ) )
75	74	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) : ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ⟶ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ) )
76		simprr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) )
77	75 76	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ∈ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ) )
78		simprl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
79	8 78	nat1st2nd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → 𝑎 ∈ ( ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ) )
80	8 79 5 24 65	natcl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ( 𝑎 ‘ 𝑣 ) ∈ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) )
81	22 24 7 57 64 66 72 77 80	catcocl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ) → ( ( 𝑎 ‘ 𝑣 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ) ∈ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) )
82	81	ralrimivva	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∀ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ( ( 𝑎 ‘ 𝑣 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ) ∈ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) )
83		eqid	⊢ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) , ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ) ) = ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) , ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ) )
84	83	fmpo	⊢ ( ∀ 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∀ ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ( ( 𝑎 ‘ 𝑣 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ) ∈ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ↔ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) , ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ) ) : ( ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) × ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ⟶ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) )
85	82 84	sylib	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) , ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ) ) : ( ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) × ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ⟶ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) )
86	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
87		eqid	⊢ ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) = ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ )
88	1 86 56 5 6 7 8 58 67 62 73 87	evlf2	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) = ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) , ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ) ) )
89	88	feq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) × ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ⟶ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ↔ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) , ℎ ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ↦ ( ( 𝑎 ‘ 𝑣 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑣 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑣 ) ‘ ℎ ) ) ) : ( ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) × ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ⟶ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ) )
90	85 89	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) × ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ⟶ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) )
91	2 8	fuchom	⊢ ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 )
92	19 20 5 91 6 58 62 67 73 23	xpchom2	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) = ( ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) × ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) )
93	1 86 56 5 58 62	evlf1	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) = ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) )
94	1 86 56 5 67 73	evlf1	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) = ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) )
95	93 94	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) = ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) )
96	92 95	feq23d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) ↔ ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) × ( 𝑢 ( Hom ‘ 𝐶 ) 𝑣 ) ) ⟶ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑣 ) ) ) )
97	90 96	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑣 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) )
98	97	ralrimivva	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑣 ∈ ( Base ‘ 𝐶 ) ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) )
99	98	ralrimivva	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑢 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑣 ∈ ( Base ‘ 𝐶 ) ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) )
100		oveq2	⊢ ( 𝑦 = ⟨ 𝑔 , 𝑣 ⟩ → ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) )
101		oveq2	⊢ ( 𝑦 = ⟨ 𝑔 , 𝑣 ⟩ → ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) )
102		fveq2	⊢ ( 𝑦 = ⟨ 𝑔 , 𝑣 ⟩ → ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝑔 , 𝑣 ⟩ ) )
103		df-ov	⊢ ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝑔 , 𝑣 ⟩ )
104	102 103	eqtr4di	⊢ ( 𝑦 = ⟨ 𝑔 , 𝑣 ⟩ → ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) = ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) )
105	104	oveq2d	⊢ ( 𝑦 = ⟨ 𝑔 , 𝑣 ⟩ → ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ) = ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) )
106	100 101 105	feq123d	⊢ ( 𝑦 = ⟨ 𝑔 , 𝑣 ⟩ → ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ) ↔ ( 𝑥 ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) ) )
107	106	ralxp	⊢ ( ∀ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ) ↔ ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑣 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) )
108		oveq1	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( 𝑥 ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) = ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) )
109		oveq1	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) = ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) )
110		fveq2	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) )
111		df-ov	⊢ ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝑓 , 𝑢 ⟩ )
112	110 111	eqtr4di	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) = ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) )
113	112	oveq1d	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) = ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) )
114	108 109 113	feq123d	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ( 𝑥 ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) ↔ ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) ) )
115	114	2ralbidv	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑣 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) ↔ ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑣 ∈ ( Base ‘ 𝐶 ) ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) ) )
116	107 115	bitrid	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ∀ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ) ↔ ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑣 ∈ ( Base ‘ 𝐶 ) ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) ) )
117	116	ralxp	⊢ ( ∀ 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∀ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ) ↔ ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑢 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑣 ∈ ( Base ‘ 𝐶 ) ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑔 , 𝑣 ⟩ ) : ( ⟨ 𝑓 , 𝑢 ⟩ ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ 𝑔 , 𝑣 ⟩ ) ⟶ ( ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ( Hom ‘ 𝐷 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑣 ) ) )
118	99 117	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∀ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ) )
119	118	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) → ∀ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ) )
120	119	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ) )
121	120	anasss	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) : ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ) )
122	28	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑄 ∈ Cat )
123	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
124		eqid	⊢ ( Id ‘ 𝑄 ) = ( Id ‘ 𝑄 )
125		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
126		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
127		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
128	19 122 123 20 5 124 125 25 126 127	xpcid	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) = ⟨ ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ⟩ )
129	128	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) ) = ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ⟩ ) )
130		df-ov	⊢ ( ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ) = ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ⟩ )
131	129 130	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) ) = ( ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ) )
132	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐷 ∈ Cat )
133		eqid	⊢ ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) = ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ )
134	20 91 124 122 126	catidcl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑓 ) )
135	5 6 125 123 127	catidcl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ∈ ( 𝑢 ( Hom ‘ 𝐶 ) 𝑢 ) )
136	1 123 132 5 6 7 8 126 126 127 127 133 134 135	evlf2val	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ) = ( ( ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) ‘ 𝑢 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑢 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ) ) )
137	30 126 32	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑓 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑓 ) )
138	5 22 137	funcf1	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
139	138 127	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ∈ ( Base ‘ 𝐷 ) )
140	22 24 26 132 139	catidcl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ∈ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) )
141	22 24 26 132 139 7 139 140	catlid	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) )
142	2 124 26 126	fucid	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) = ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝑓 ) ) )
143	142	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) ‘ 𝑢 ) = ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝑓 ) ) ‘ 𝑢 ) )
144		fvco3	⊢ ( ( ( 1^st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝑓 ) ) ‘ 𝑢 ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) )
145	138 127 144	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝑓 ) ) ‘ 𝑢 ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) )
146	143 145	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) ‘ 𝑢 ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) )
147	5 125 26 137 127	funcid	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑢 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) )
148	146 147	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) ‘ 𝑢 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑢 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ) ) = ( ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ) )
149	1 123 132 5 126 127	evlf1	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) = ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) )
150	149	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) )
151	141 148 150	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( Id ‘ 𝑄 ) ‘ 𝑓 ) ‘ 𝑢 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) , ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑢 ) ) ( ( 𝑢 ( 2^nd ‘ 𝑓 ) 𝑢 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑢 ) ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ) )
152	131 136 151	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑢 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ) )
153	152	ralrimivva	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑢 ∈ ( Base ‘ 𝐶 ) ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ) )
154		id	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ )
155	154 154	oveq12d	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑥 ) = ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) )
156		fveq2	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ 𝑥 ) = ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) )
157	155 156	fveq12d	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑥 ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ 𝑥 ) ) = ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) ) )
158	112	fveq2d	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ) )
159	157 158	eqeq12d	⊢ ( 𝑥 = ⟨ 𝑓 , 𝑢 ⟩ → ( ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑥 ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ) ↔ ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ) ) )
160	159	ralxp	⊢ ( ∀ 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑥 ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ) ↔ ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑢 ∈ ( Base ‘ 𝐶 ) ( ( ⟨ 𝑓 , 𝑢 ⟩ ( 2^nd ‘ 𝐸 ) ⟨ 𝑓 , 𝑢 ⟩ ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ ⟨ 𝑓 , 𝑢 ⟩ ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ( 1^st ‘ 𝐸 ) 𝑢 ) ) )
161	153 160	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑥 ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ) )
162	161	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑥 ) ‘ ( ( Id ‘ ( 𝑄 ×_c 𝐶 ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) ) )
163	3	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
164	4	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝐷 ∈ Cat )
165		simp21	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) )
166		1st2nd2	⊢ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
167	165 166	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
168	167 165	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) )
169		opelxp	⊢ ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑥 ) ∈ ( 𝐶 Func 𝐷 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) ) )
170	168 169	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝑥 ) ∈ ( 𝐶 Func 𝐷 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) ) )
171		simp22	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) )
172		1st2nd2	⊢ ( 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
173	171 172	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
174	173 171	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) )
175		opelxp	⊢ ( ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑦 ) ∈ ( 𝐶 Func 𝐷 ) ∧ ( 2^nd ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) ) )
176	174 175	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝑦 ) ∈ ( 𝐶 Func 𝐷 ) ∧ ( 2^nd ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) ) )
177		simp23	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) )
178		1st2nd2	⊢ ( 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
179	177 178	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
180	179 177	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) )
181		opelxp	⊢ ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑧 ) ∈ ( 𝐶 Func 𝐷 ) ∧ ( 2^nd ‘ 𝑧 ) ∈ ( Base ‘ 𝐶 ) ) )
182	180 181	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝑧 ) ∈ ( 𝐶 Func 𝐷 ) ∧ ( 2^nd ‘ 𝑧 ) ∈ ( Base ‘ 𝐶 ) ) )
183		simp3l	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) )
184	19 21 91 6 23 165 171	xpchom	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) = ( ( ( 1^st ‘ 𝑥 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑦 ) ) × ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) )
185	183 184	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑓 ∈ ( ( ( 1^st ‘ 𝑥 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑦 ) ) × ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) )
186		1st2nd2	⊢ ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑥 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑦 ) ) × ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) → 𝑓 = ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ )
187	185 186	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑓 = ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ )
188	187 185	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ∈ ( ( ( 1^st ‘ 𝑥 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑦 ) ) × ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) )
189		opelxp	⊢ ( ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ∈ ( ( ( 1^st ‘ 𝑥 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑦 ) ) × ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ↔ ( ( 1^st ‘ 𝑓 ) ∈ ( ( 1^st ‘ 𝑥 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑦 ) ) ∧ ( 2^nd ‘ 𝑓 ) ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) )
190	188 189	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝑓 ) ∈ ( ( 1^st ‘ 𝑥 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑦 ) ) ∧ ( 2^nd ‘ 𝑓 ) ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) )
191		simp3r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) )
192	19 21 91 6 23 171 177	xpchom	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) = ( ( ( 1^st ‘ 𝑦 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑧 ) ) × ( ( 2^nd ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) )
193	191 192	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑔 ∈ ( ( ( 1^st ‘ 𝑦 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑧 ) ) × ( ( 2^nd ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) )
194		1st2nd2	⊢ ( 𝑔 ∈ ( ( ( 1^st ‘ 𝑦 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑧 ) ) × ( ( 2^nd ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) → 𝑔 = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
195	193 194	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → 𝑔 = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
196	195 193	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ∈ ( ( ( 1^st ‘ 𝑦 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑧 ) ) × ( ( 2^nd ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) )
197		opelxp	⊢ ( ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ∈ ( ( ( 1^st ‘ 𝑦 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑧 ) ) × ( ( 2^nd ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) ↔ ( ( 1^st ‘ 𝑔 ) ∈ ( ( 1^st ‘ 𝑦 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑧 ) ) ∧ ( 2^nd ‘ 𝑔 ) ∈ ( ( 2^nd ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) )
198	196 197	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝑔 ) ∈ ( ( 1^st ‘ 𝑦 ) ( 𝐶 Nat 𝐷 ) ( 1^st ‘ 𝑧 ) ) ∧ ( 2^nd ‘ 𝑔 ) ∈ ( ( 2^nd ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) )
199	1 2 163 164 8 170 176 182 190 198	evlfcllem	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ‘ ( ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ( ⟨ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ , ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) ) = ( ( ( ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) , ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ) ( ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) ) )
200	167 179	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑧 ) = ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
201	167 173	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ , ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ⟩ )
202	201 179	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) = ( ⟨ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ , ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
203	202 195 187	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) 𝑓 ) = ( ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ( ⟨ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ , ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) )
204	200 203	fveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) 𝑓 ) ) = ( ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ‘ ( ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ( ⟨ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ , ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) ) )
205	167	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
206	173	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) )
207	205 206	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ⟨ ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) , ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) ⟩ )
208	179	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
209	207 208	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) = ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) , ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ) )
210	173 179	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( 𝑦 ( 2^nd ‘ 𝐸 ) 𝑧 ) = ( ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
211	210 195	fveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐸 ) 𝑧 ) ‘ 𝑔 ) = ( ( ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ) )
212	167 173	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) = ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) )
213	212 187	fveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) ‘ 𝑓 ) = ( ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) )
214	209 211 213	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝐸 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) , ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) ) ( ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) ) )
215	199 204 214	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 𝐶 Func 𝐷 ) × ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝑄 ×_c 𝐶 ) ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐸 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝐸 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐸 ) 𝑦 ) ‘ 𝑓 ) ) )
216	21 22 23 24 25 26 27 7 29 4 44 55 121 162 215	isfuncd	⊢ ( 𝜑 → ( 1^st ‘ 𝐸 ) ( ( 𝑄 ×_c 𝐶 ) Func 𝐷 ) ( 2^nd ‘ 𝐸 ) )
217		df-br	⊢ ( ( 1^st ‘ 𝐸 ) ( ( 𝑄 ×_c 𝐶 ) Func 𝐷 ) ( 2^nd ‘ 𝐸 ) ↔ ⟨ ( 1^st ‘ 𝐸 ) , ( 2^nd ‘ 𝐸 ) ⟩ ∈ ( ( 𝑄 ×_c 𝐶 ) Func 𝐷 ) )
218	216 217	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐸 ) , ( 2^nd ‘ 𝐸 ) ⟩ ∈ ( ( 𝑄 ×_c 𝐶 ) Func 𝐷 ) )
219	18 218	eqeltrd	⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑄 ×_c 𝐶 ) Func 𝐷 ) )

Metamath Proof Explorer

Theorem evlfcl

Proof