Metamath Proof Explorer

Theorem 2ndfcl

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

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

Proof

Step Hyp Ref Expression
1 1stfcl.t ⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2 1stfcl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
3 1stfcl.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
4 2ndfcl.p ⊢ 𝑄 = ( 𝐶 2ndF 𝐷 )
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 2ndfval ⊢ ( 𝜑 → 𝑄 = ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ⟩ )
10 fo2nd ⊢ 2nd : V –onto→ V
11 fofun ⊢ ( 2nd : V –onto→ V → Fun 2nd )
12 10 11 ax-mp ⊢ Fun 2nd
13 fvex ⊢ ( Base ‘ 𝐶 ) ∈ V
14 fvex ⊢ ( Base ‘ 𝐷 ) ∈ V
15 13 14 xpex ⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∈ V
16 resfunexg ⊢ ( ( Fun 2nd ∧ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∈ V ) → ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∈ V )
17 12 15 16 mp2an ⊢ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∈ V
18 15 15 mpoex ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ∈ V
19 17 18 op2ndd ⊢ ( 𝑄 = ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ⟩ → ( 2nd ‘ 𝑄 ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) )
20 9 19 syl ⊢ ( 𝜑 → ( 2nd ‘ 𝑄 ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) )
21 20 opeq2d ⊢ ( 𝜑 → ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑄 ) ⟩ = ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) ⟩ )
22 9 21 eqtr4d ⊢ ( 𝜑 → 𝑄 = ⟨ ( 2nd ↾ ( ( 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 f2ndres ⊢ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐷 )
30 29 a1i ⊢ ( 𝜑 → ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐷 ) )
31 eqid ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) )
32 ovex ⊢ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∈ V
33 resfunexg ⊢ ( ( Fun 2nd ∧ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∈ V ) → ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ∈ V )
34 12 32 33 mp2an ⊢ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ∈ V
35 31 34 fnmpoi ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
36 20 fneq1d ⊢ ( 𝜑 → ( ( 2nd ‘ 𝑄 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ↔ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) )
37 35 36 mpbiri ⊢ ( 𝜑 → ( 2nd ‘ 𝑄 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) )
38 f2ndres ⊢ ( 2nd ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) )
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 2ndf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) = ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) )
44 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
45 1 7 44 23 8 41 42 xpchom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) = ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) )
46 45 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) = ( 2nd ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) )
47 43 46 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) = ( 2nd ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) )
48 47 feq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ↔ ( 2nd ↾ ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) )
49 38 48 mpbiri ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) )
50 fvres ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 2nd ‘ 𝑥 ) )
51 50 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 2nd ‘ 𝑥 ) )
52 fvres ⊢ ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) = ( 2nd ‘ 𝑦 ) )
53 52 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) = ( 2nd ‘ 𝑦 ) )
54 51 53 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) = ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) )
55 45 54 feq23d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ⟶ ( ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) ↔ ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) : ( ( ( 1st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑦 ) ) × ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) ⟶ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑦 ) ) ) )
56 49 55 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ⟶ ( ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 2nd ↾ ( ( 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 ‘ 𝐷 ) ) ) → ( ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( 2nd ‘ ( ( 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 66 25 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 op2ndd ⊢ ( ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ ( 1st ‘ 𝑥 ) ) , ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ → ( 2nd ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) )
76 72 75 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 2nd ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) )
77 60 76 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) )
78 1 7 8 64 65 4 58 58 2ndf2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑥 ) = ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) )
79 78 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑥 ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑥 ) ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) )
80 50 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 2nd ‘ 𝑥 ) )
81 80 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( Id ‘ 𝐷 ) ‘ ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 2nd ‘ 𝑥 ) ) )
82 77 79 81 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑥 ) ‘ ( ( Id ‘ 𝑇 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 2nd ↾ ( ( 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 ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( 2nd ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) )
91 1 7 8 26 84 85 86 87 88 27 xpcco2nd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 2nd ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( 2nd ‘ 𝑔 ) ( ⟨ ( 2nd ‘ 𝑥 ) , ( 2nd ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) ( 2nd ‘ 𝑓 ) ) )
92 90 91 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( 2nd ‘ 𝑔 ) ( ⟨ ( 2nd ‘ 𝑥 ) , ( 2nd ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) ( 2nd ‘ 𝑓 ) ) )
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 2ndf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑧 ) = ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) )
96 95 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) )
97 84 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( 2nd ‘ 𝑥 ) )
98 85 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) = ( 2nd ‘ 𝑦 ) )
99 97 98 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ⟨ ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ = ⟨ ( 2nd ‘ 𝑥 ) , ( 2nd ‘ 𝑦 ) ⟩ )
100 86 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
101 99 100 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ⟨ ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) ) = ( ⟨ ( 2nd ‘ 𝑥 ) , ( 2nd ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) )
102 1 7 8 93 94 4 85 86 2ndf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑦 ( 2nd ‘ 𝑄 ) 𝑧 ) = ( 2nd ↾ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) )
103 102 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝑄 ) 𝑧 ) ‘ 𝑔 ) = ( ( 2nd ↾ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ 𝑔 ) )
104 88 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 2nd ↾ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ‘ 𝑔 ) = ( 2nd ‘ 𝑔 ) )
105 103 104 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2nd ‘ 𝑄 ) 𝑧 ) ‘ 𝑔 ) = ( 2nd ‘ 𝑔 ) )
106 1 7 8 93 94 4 84 85 2ndf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) = ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) )
107 106 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) ‘ 𝑓 ) = ( ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ‘ 𝑓 ) )
108 87 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 2nd ↾ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ) ‘ 𝑓 ) = ( 2nd ‘ 𝑓 ) )
109 107 108 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) ‘ 𝑓 ) = ( 2nd ‘ 𝑓 ) )
110 101 105 109 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2nd ‘ 𝑄 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 2nd ‘ 𝑔 ) ( ⟨ ( 2nd ‘ 𝑥 ) , ( 2nd ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) ( 2nd ‘ 𝑓 ) ) )
111 92 96 110 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑇 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑇 ) 𝑧 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑇 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 ( 2nd ‘ 𝑄 ) 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑥 ) , ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ‘ 𝑧 ) ) ( ( 𝑥 ( 2nd ‘ 𝑄 ) 𝑦 ) ‘ 𝑓 ) ) )
112 7 6 8 23 24 25 26 27 28 3 30 37 56 82 111 isfuncd ⊢ ( 𝜑 → ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ( 𝑇 Func 𝐷 ) ( 2nd ‘ 𝑄 ) )
113 df-br ⊢ ( ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ( 𝑇 Func 𝐷 ) ( 2nd ‘ 𝑄 ) ↔ ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑄 ) ⟩ ∈ ( 𝑇 Func 𝐷 ) )
114 112 113 sylib ⊢ ( 𝜑 → ⟨ ( 2nd ↾ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) , ( 2nd ‘ 𝑄 ) ⟩ ∈ ( 𝑇 Func 𝐷 ) )
115 22 114 eqeltrd ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑇 Func 𝐷 ) )