Metamath Proof Explorer

Theorem 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 ⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
curfcl.q ⊢ 𝑄 = ( 𝐷 FuncCat 𝐸 )
curfcl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
curfcl.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
curfcl.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
Assertion curfcl ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝑄 ) )

Proof

Step Hyp Ref Expression
1 curfcl.g ⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
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 ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
13 fvex ⊢ ( Base ‘ 𝐶 ) ∈ V
14 13 mptex ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) ∈ V
15 13 13 mpoex ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ∈ V
16 14 15 op1std ⊢ ( 𝐺 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ → ( 1st ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )
17 12 16 syl ⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )
18 14 15 op2ndd ⊢ ( 𝐺 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ → ( 2nd ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) )
19 12 18 syl ⊢ ( 𝜑 → ( 2nd ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) )
20 17 19 opeq12d ⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
21 12 20 eqtr4d ⊢ ( 𝜑 → 𝐺 = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
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 ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ∈ V
33 32 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ∈ V )
34 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
35 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
36 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
38 eqid ⊢ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1st ‘ 𝐺 ) ‘ 𝑥 )
39 1 6 34 35 36 7 37 38 curf1cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) )
40 33 17 39 fmpt2d ⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( 𝐷 Func 𝐸 ) )
41 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
42 ovex ⊢ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∈ V
43 42 mptex ⊢ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ∈ V
44 41 43 fnmpoi ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
45 19 fneq1d ⊢ ( 𝜑 → ( ( 2nd ‘ 𝐺 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
46 44 45 mpbiri ⊢ ( 𝜑 → ( 2nd ‘ 𝐺 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
47 fvex ⊢ ( Base ‘ 𝐷 ) ∈ V
48 47 mptex ⊢ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ∈ V
49 48 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ∈ V )
50 19 oveqd ⊢ ( 𝜑 → ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) 𝑦 ) )
51 41 ovmpt4g ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ∈ V ) → ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) 𝑦 ) = ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
52 43 51 mp3an3 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) 𝑦 ) = ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
53 50 52 sylan9eq ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) = ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( 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 ⊢ ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) = ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 )
61 1 6 54 55 56 7 10 11 57 58 59 60 23 curf2cl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑔 ) ∈ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) )
62 49 53 61 fmpt2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) )
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 𝐸 ) ) → ( 1st ‘ 𝐹 ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
69 67 5 68 sylancr ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
70 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
71 opelxpi ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
72 71 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
73 64 65 66 70 72 funcid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ( ( Id ‘ ( 𝐶 ×c 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
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 ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ( ( Id ‘ ( 𝐶 ×c 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ⟩ ) )
80 df-ov ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ⟩ )
81 79 80 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ‘ ( ( Id ‘ ( 𝐶 ×c 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) )
82 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
83 1 6 74 75 82 7 76 38 77 curf11 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) = ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) )
84 df-ov ⊢ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) = ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
85 83 84 eqtr2di ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) )
86 85 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) )
87 73 81 86 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) )
88 87 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) ) )
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 𝐸 ) ∧ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐸 ) ) → ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) )
97 95 39 96 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) )
98 7 90 97 funcf1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
99 fcompt ⊢ ( ( ( Id ‘ 𝐸 ) : ( Base ‘ 𝐸 ) ⟶ V ∧ ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) ) → ( ( Id ‘ 𝐸 ) ∘ ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) ) )
100 94 98 99 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐸 ) ∘ ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) ) ) )
101 88 100 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) ) = ( ( Id ‘ 𝐸 ) ∘ ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
102 6 10 9 34 37 catidcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
103 eqid ⊢ ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
104 1 6 34 35 36 7 10 11 37 37 102 103 curf2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑦 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ) ) )
105 2 25 66 39 fucid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑄 ) ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ∘ ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
106 101 104 105 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑄 ) ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) )
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 ‘ 𝐷 ) ) → ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) = ( 𝑥 ( 1st ‘ 𝐹 ) 𝑤 ) )
117 df-ov ⊢ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑤 ) = ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ )
118 116 117 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) = ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) )
119 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
120 119 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
121 eqid ⊢ ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) = ( ( 1st ‘ 𝐺 ) ‘ 𝑦 )
122 1 6 108 110 112 7 120 121 115 curf11 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) = ( 𝑦 ( 1st ‘ 𝐹 ) 𝑤 ) )
123 df-ov ⊢ ( 𝑦 ( 1st ‘ 𝐹 ) 𝑤 ) = ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ )
124 122 123 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) = ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) )
125 118 124 opeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ = ⟨ ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) , ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) ⟩ )
126 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
127 126 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
128 eqid ⊢ ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) = ( ( 1st ‘ 𝐺 ) ‘ 𝑧 )
129 1 6 108 110 112 7 127 128 115 curf11 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) = ( 𝑧 ( 1st ‘ 𝐹 ) 𝑤 ) )
130 df-ov ⊢ ( 𝑧 ( 1st ‘ 𝐹 ) 𝑤 ) = ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ )
131 129 130 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) = ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
132 125 131 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) , ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
133 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
134 133 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
135 eqid ⊢ ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) = ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 )
136 1 6 108 110 112 7 10 11 120 127 134 135 115 curf2val ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) )
137 df-ov ⊢ ( 𝑔 ( ⟨ 𝑦 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ⟨ 𝑦 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
138 136 137 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) = ( ( ⟨ 𝑦 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) )
139 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
140 139 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
141 eqid ⊢ ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 )
142 1 6 108 110 112 7 10 11 114 120 140 141 115 curf2val ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) )
143 df-ov ⊢ ( 𝑓 ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
144 142 143 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) )
145 132 138 144 oveq123d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) ) = ( ( ( ⟨ 𝑦 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) , ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( 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 ‘ 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
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 ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑤 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ) = ( ( ( ⟨ 𝑦 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) , ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑦 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( 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 ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑤 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) )
170 df-ov ⊢ ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
171 169 170 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑔 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑤 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ) = ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) )
172 145 163 171 3eqtr2rd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) ) )
173 172 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) ) ) )
174 6 10 26 107 113 119 126 139 133 catcocl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
175 eqid ⊢ ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
176 1 6 107 109 111 7 10 11 113 126 174 175 curf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ( ⟨ 𝑥 , 𝑤 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) ) )
177 1 6 107 109 111 7 10 11 113 119 139 141 23 curf2cl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) )
178 1 6 107 109 111 7 10 11 119 126 133 135 23 curf2cl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ( 𝐷 Nat 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) )
179 2 23 7 148 27 177 178 fucco ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑄 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) = ( 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ ( ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) , ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ‘ 𝑤 ) ) ) )
180 173 176 179 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑄 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) )
181 6 22 10 24 9 25 26 27 3 31 40 46 62 106 180 isfuncd ⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝐺 ) )
182 df-br ⊢ ( ( 1st ‘ 𝐺 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝐺 ) ↔ ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ∈ ( 𝐶 Func 𝑄 ) )
183 181 182 sylib ⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ∈ ( 𝐶 Func 𝑄 ) )
184 21 183 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝑄 ) )