Metamath Proof Explorer

Theorem prfcl

Description: The pairing of functors F : C --> D and G : C --> D is a functor <. F , G >. : C --> ( D X. E ) . (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses prfcl.p ⊢ 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
prfcl.t ⊢ 𝑇 = ( 𝐷 ×c 𝐸 )
prfcl.c ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
prfcl.d ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
Assertion prfcl ( 𝜑 → 𝑃 ∈ ( 𝐶 Func 𝑇 ) )

Proof

Step Hyp Ref Expression
1 prfcl.p ⊢ 𝑃 = ( 𝐹 ⟨,⟩F 𝐺 )
2 prfcl.t ⊢ 𝑇 = ( 𝐷 ×c 𝐸 )
3 prfcl.c ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
4 prfcl.d ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7 1 5 6 3 4 prfval ⊢ ( 𝜑 → 𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
8 fvex ⊢ ( Base ‘ 𝐶 ) ∈ V
9 8 mptex ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) ∈ V
10 8 8 mpoex ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ∈ V
11 9 10 op1std ⊢ ( 𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ → ( 1st ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
12 7 11 syl ⊢ ( 𝜑 → ( 1st ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
13 9 10 op2ndd ⊢ ( 𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ → ( 2nd ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) )
14 7 13 syl ⊢ ( 𝜑 → ( 2nd ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) )
15 12 14 opeq12d ⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
16 7 15 eqtr4d ⊢ ( 𝜑 → 𝑃 = ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ )
17 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
19 2 17 18 xpcbas ⊢ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) = ( Base ‘ 𝑇 )
20 eqid ⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
21 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
22 eqid ⊢ ( Id ‘ 𝑇 ) = ( Id ‘ 𝑇 )
23 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
24 eqid ⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 )
25 funcrcl ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
26 3 25 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
27 26 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
28 26 simprd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
29 funcrcl ⊢ ( 𝐺 ∈ ( 𝐶 Func 𝐸 ) → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
30 4 29 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
31 30 simprd ⊢ ( 𝜑 → 𝐸 ∈ Cat )
32 2 28 31 xpccat ⊢ ( 𝜑 → 𝑇 ∈ Cat )
33 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
34 1st2ndbr ⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
35 33 3 34 sylancr ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
36 5 17 35 funcf1 ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
37 36 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
38 relfunc ⊢ Rel ( 𝐶 Func 𝐸 )
39 1st2ndbr ⊢ ( ( Rel ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) → ( 1st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
40 38 4 39 sylancr ⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
41 5 18 40 funcf1 ⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
42 41 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
43 37 42 opelxpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
44 12 43 fmpt3d ⊢ ( 𝜑 → ( 1st ‘ 𝑃 ) : ( Base ‘ 𝐶 ) ⟶ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
45 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
46 ovex ⊢ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∈ V
47 46 mptex ⊢ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ∈ V
48 45 47 fnmpoi ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
49 14 fneq1d ⊢ ( 𝜑 → ( ( 2nd ‘ 𝑃 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
50 48 49 mpbiri ⊢ ( 𝜑 → ( 2nd ‘ 𝑃 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
51 14 oveqd ⊢ ( 𝜑 → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) 𝑦 ) )
52 45 ovmpt4g ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ∈ V ) → ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) 𝑦 ) = ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
53 47 52 mp3an3 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) 𝑦 ) = ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
54 51 53 sylan9eq ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) = ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) )
55 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
56 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
57 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
58 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
59 5 6 55 56 57 58 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) )
60 59 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) ∈ ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) )
61 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
62 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
63 5 6 61 62 57 58 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) )
64 63 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ∈ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) )
65 60 64 opelxpd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ∈ ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) × ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
66 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
67 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
68 1 5 6 66 67 57 prf1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) = ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ )
69 1 5 6 66 67 58 prf1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) = ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ )
70 68 69 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ) = ( ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( Hom ‘ 𝑇 ) ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ) )
71 37 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
72 42 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
73 36 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
74 73 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
75 41 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐸 ) )
76 75 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐸 ) )
77 2 17 18 55 61 71 72 74 76 20 xpchom2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( Hom ‘ 𝑇 ) ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ) = ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) × ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
78 70 77 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ) = ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) × ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
79 78 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ) = ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) × ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
80 65 79 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ∈ ( ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ) )
81 54 80 fmpt3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ) )
82 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
83 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
84 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
85 5 21 82 83 84 funcid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) )
86 eqid ⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
87 40 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
88 5 21 86 87 84 funcid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) )
89 85 88 opeq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ⟩ = ⟨ ( ( Id ‘ 𝐷 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ )
90 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
91 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
92 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
93 5 6 21 92 84 catidcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
94 1 5 6 90 91 84 84 93 prf2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ⟩ )
95 1 5 6 90 91 84 prf1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) = ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ )
96 95 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑇 ) ‘ ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑇 ) ‘ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
97 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
98 31 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
99 2 97 98 17 18 82 86 22 37 42 xpcid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑇 ) ‘ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) = ⟨ ( ( Id ‘ 𝐷 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ )
100 96 99 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑇 ) ‘ ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) ) = ⟨ ( ( Id ‘ 𝐷 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( Id ‘ 𝐸 ) ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) ⟩ )
101 89 94 100 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑇 ) ‘ ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) ) )
102 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
103 35 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
104 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
105 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
106 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
107 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
108 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
109 5 6 23 102 103 104 105 106 107 108 funcco ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
110 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
111 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
112 38 111 39 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
113 5 6 23 110 112 104 105 106 107 108 funcco ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) )
114 109 113 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ⟩ = ⟨ ( ( ( 𝑦 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) , ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) ⟩ )
115 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
116 27 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
117 5 6 23 116 104 105 106 107 108 catcocl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
118 1 5 6 115 111 104 106 117 prf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) ⟩ )
119 1 5 6 115 111 104 prf1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) = ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ )
120 1 5 6 115 111 105 prf1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) = ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ )
121 119 120 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ⟨ ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ = ⟨ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ , ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ⟩ )
122 1 5 6 115 111 106 prf1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1st ‘ 𝑃 ) ‘ 𝑧 ) = ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ )
123 121 122 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ⟨ ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑃 ) ‘ 𝑧 ) ) = ( ⟨ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ , ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ 𝑇 ) ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ) )
124 1 5 6 115 111 105 106 108 prf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) = ⟨ ( ( 𝑦 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) , ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ⟩ )
125 1 5 6 115 111 104 105 107 prf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) = ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ )
126 123 124 125 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑃 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ⟨ ( ( 𝑦 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) , ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ⟩ ( ⟨ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ , ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ 𝑇 ) ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ) ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ ) )
127 36 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
128 127 104 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
129 41 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
130 129 104 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
131 127 105 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
132 129 105 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐸 ) )
133 127 106 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
134 129 106 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐸 ) )
135 5 6 55 103 104 105 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) )
136 135 107 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ) )
137 5 6 61 112 104 105 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) )
138 137 107 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ) )
139 5 6 55 103 105 106 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑦 ( 2nd ‘ 𝐹 ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ⟶ ( ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) ) )
140 139 108 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) ) )
141 5 6 61 112 105 106 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ⟶ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) )
142 141 108 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) )
143 2 17 18 55 61 128 130 131 132 102 110 24 133 134 136 138 140 142 xpcco2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ⟨ ( ( 𝑦 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) , ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ⟩ ( ⟨ ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ , ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ⟩ ( comp ‘ 𝑇 ) ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ) ⟨ ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ ) = ⟨ ( ( ( 𝑦 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) , ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) ⟩ )
144 126 143 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑃 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ⟨ ( ( ( 𝑦 ( 2nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) , ( ( ( 𝑦 ( 2nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ) ⟩ )
145 114 118 144 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ‘ 𝑃 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑃 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st ‘ 𝑃 ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) )
146 5 19 6 20 21 22 23 24 27 32 44 50 81 101 145 isfuncd ⊢ ( 𝜑 → ( 1st ‘ 𝑃 ) ( 𝐶 Func 𝑇 ) ( 2nd ‘ 𝑃 ) )
147 df-br ⊢ ( ( 1st ‘ 𝑃 ) ( 𝐶 Func 𝑇 ) ( 2nd ‘ 𝑃 ) ↔ ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ ∈ ( 𝐶 Func 𝑇 ) )
148 146 147 sylib ⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝑃 ) , ( 2nd ‘ 𝑃 ) ⟩ ∈ ( 𝐶 Func 𝑇 ) )
149 16 148 eqeltrd ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐶 Func 𝑇 ) )