This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1stfcl

Description: The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses 1stfcl.t ⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
1stfcl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
1stfcl.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
1stfcl.p ⊢ 𝑃 = ( 𝐶 1stF 𝐷 )
Assertion 1stfcl ( 𝜑 → 𝑃 ∈ ( 𝑇 Func 𝐶 ) )

Proof

Step Hyp Ref Expression
1 1stfcl.t ⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2 1stfcl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
3 1stfcl.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
4 1stfcl.p ⊢ 𝑃 = ( 𝐶 1stF 𝐷 )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7 1 5 6 xpcbas ⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑇 )
8 eqid ⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
9 1 7 8 2 3 4 1stfval ⊢ ( 𝜑 → 𝑃 = ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ⟩ )
10 fo1st ⊢ 1st : V –onto→ V
11 fofun ⊢ ( 1st : V –onto→ V → Fun 1st )
12 10 11 ax-mp ⊢ Fun 1st
13 fvex ⊢ ( Base ‘ 𝐶 ) ∈ V
14 fvex ⊢ ( Base ‘ 𝐷 ) ∈ V
15 13 14 xpex ⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∈ V
16 resfunexg ⊢ ( ( Fun 1st ∧ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∈ V ) → ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∈ V )
17 12 15 16 mp2an ⊢ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∈ V
18 15 15 mpoex ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ∈ V
19 17 18 op2ndd ⊢ ( 𝑃 = ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ⟩ → ( 2nd ‘ 𝑃 ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) )
20 9 19 syl ⊢ ( 𝜑 → ( 2nd ‘ 𝑃 ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) )
21 20 opeq2d ⊢ ( 𝜑 → ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑃 ) ⟩ = ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ⟩ )
22 9 21 eqtr4d ⊢ ( 𝜑 → 𝑃 = ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑃 ) ⟩ )
23 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
24 eqid ⊢ ( Id ‘ 𝑇 ) = ( Id ‘ 𝑇 )
25 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
26 eqid ⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 )
27 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
28 1 2 3 xpccat ⊢ ( 𝜑 → 𝑇 ∈ Cat )
29 f1stres ⊢ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐶 )
30 29 a1i ⊢ ( 𝜑 → ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐶 ) )
31 eqid ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) )
32 ovex ⊢ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∈ V
33 resfunexg ⊢ ( ( Fun 1st ∧ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∈ V ) → ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ∈ V )
34 12 32 33 mp2an ⊢ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ∈ V
35 31 34 fnmpoi ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
36 20 fneq1d ⊢ ( 𝜑 → ( ( 2nd ‘ 𝑃 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ↔ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) )
37 35 36 mpbiri ⊢ ( 𝜑 → ( 2nd ‘ 𝑃 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) )
38 f1stres ⊢ ( 1st ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) )
39 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → 𝐶 ∈ Cat )
40 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → 𝐷 ∈ Cat )
41 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
42 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
43 1 7 8 39 40 4 41 42 1stf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) = ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) )
44 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
45 1 7 23 44 8 41 42 xpchom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) = ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) )
46 45 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) = ( 1st ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) )
47 43 46 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) = ( 1st ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) )
48 47 feq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) ↔ ( 1st ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) ) )
49 38 48 mpbiri ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) )
50 fvres ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 1st ‘ 𝑥 ) )
51 50 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 1st ‘ 𝑥 ) )
52 fvres ⊢ ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) = ( 1st ‘ 𝑦 ) )
53 52 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) = ( 1st ‘ 𝑦 ) )
54 51 53 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) = ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) )
55 45 54 feq23d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ⟶ ( ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) ↔ ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) ) )
56 49 55 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ⟶ ( ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) )
57 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝑇 ∈ Cat )
58 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
59 7 8 24 57 58 catidcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) )
60 59 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( 1st ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) )
61 1st2nd2 ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
62 61 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
63 62 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) = ( ( Id ‘ 𝑇 ) ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) )
64 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝐶 ∈ Cat )
65 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → 𝐷 ∈ Cat )
66 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
67 xp1st ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 1st ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 1st ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
69 xp2nd ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 2nd ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 2nd ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
71 1 64 65 5 6 25 66 24 68 70 xpcid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝑇 ) ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) , ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ )
72 63 71 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) , ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ )
73 fvex ⊢ ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) ∈ V
74 fvex ⊢ ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) ∈ V
75 73 74 op1std ⊢ ( ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) , ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ → ( 1st ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) )
76 72 75 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 1st ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) )
77 60 76 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) )
78 1 7 8 64 65 4 58 58 1stf2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑥 ) = ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) )
79 78 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑥 ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) )
80 50 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 1st ‘ 𝑥 ) )
81 80 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) )
82 77 79 81 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑥 ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ) )
83 28 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑇 ∈ Cat )
84 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
85 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
86 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
87 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) )
88 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) )
89 7 8 26 83 84 85 86 87 88 catcocl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) )
90 89 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( 1st ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) )
91 1 7 8 26 84 85 86 87 88 27 xpcco1st ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 1st ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( 1st ‘ 𝑔 ) ( ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑧 ) ) ( 1st ‘ 𝑓 ) ) )
92 90 91 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( 1st ‘ 𝑔 ) ( ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑧 ) ) ( 1st ‘ 𝑓 ) ) )
93 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
94 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → 𝐷 ∈ Cat )
95 1 7 8 93 94 4 84 86 1stf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑧 ) = ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) )
96 95 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) )
97 84 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 1st ‘ 𝑥 ) )
98 85 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) = ( 1st ‘ 𝑦 ) )
99 97 98 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ⟨ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ = ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ )
100 86 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) = ( 1st ‘ 𝑧 ) )
101 99 100 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ⟨ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) ) = ( ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑧 ) ) )
102 1 7 8 93 94 4 85 86 1stf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) = ( 1st ↾ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) )
103 102 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) = ( ( 1st ↾ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ 𝑔 ) )
104 88 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ 𝑔 ) = ( 1st ‘ 𝑔 ) )
105 103 104 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) = ( 1st ‘ 𝑔 ) )
106 1 7 8 93 94 4 84 85 1stf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) = ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) )
107 106 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) = ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ‘ 𝑓 ) )
108 87 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 1st ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ‘ 𝑓 ) = ( 1st ‘ 𝑓 ) )
109 107 108 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) = ( 1st ‘ 𝑓 ) )
110 101 105 109 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 1st ‘ 𝑔 ) ( ⟨ ( 1st ‘ 𝑥 ) , ( 1st ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑧 ) ) ( 1st ‘ 𝑓 ) ) )
111 92 96 110 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝑃 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) )
112 7 5 8 23 24 25 26 27 28 2 30 37 56 82 111 isfuncd ⊢ ( 𝜑 → ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ( 𝑇 Func 𝐶 ) ( 2nd ‘ 𝑃 ) )
113 df-br ⊢ ( ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ( 𝑇 Func 𝐶 ) ( 2nd ‘ 𝑃 ) ↔ ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑃 ) ⟩ ∈ ( 𝑇 Func 𝐶 ) )
114 112 113 sylib ⊢ ( 𝜑 → ⟨ ( 1st ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑃 ) ⟩ ∈ ( 𝑇 Func 𝐶 ) )
115 22 114 eqeltrd ⊢ ( 𝜑 → 𝑃 ∈ ( 𝑇 Func 𝐶 ) )