Metamath Proof Explorer


Definition df-xpc

Description: Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Assertion df-xpc ×c = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ( 𝑢𝑏 , 𝑣𝑏 ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) ) ) / { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxpc ×c
1 vr 𝑟
2 cvv V
3 vs 𝑠
4 cbs Base
5 1 cv 𝑟
6 5 4 cfv ( Base ‘ 𝑟 )
7 3 cv 𝑠
8 7 4 cfv ( Base ‘ 𝑠 )
9 6 8 cxp ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) )
10 vb 𝑏
11 vu 𝑢
12 10 cv 𝑏
13 vv 𝑣
14 c1st 1st
15 11 cv 𝑢
16 15 14 cfv ( 1st𝑢 )
17 chom Hom
18 5 17 cfv ( Hom ‘ 𝑟 )
19 13 cv 𝑣
20 19 14 cfv ( 1st𝑣 )
21 16 20 18 co ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) )
22 c2nd 2nd
23 15 22 cfv ( 2nd𝑢 )
24 7 17 cfv ( Hom ‘ 𝑠 )
25 19 22 cfv ( 2nd𝑣 )
26 23 25 24 co ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) )
27 21 26 cxp ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) )
28 11 13 12 12 27 cmpo ( 𝑢𝑏 , 𝑣𝑏 ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) ) )
29 vh
30 cnx ndx
31 30 4 cfv ( Base ‘ ndx )
32 31 12 cop ⟨ ( Base ‘ ndx ) , 𝑏
33 30 17 cfv ( Hom ‘ ndx )
34 29 cv
35 33 34 cop ⟨ ( Hom ‘ ndx ) ,
36 cco comp
37 30 36 cfv ( comp ‘ ndx )
38 vx 𝑥
39 12 12 cxp ( 𝑏 × 𝑏 )
40 vy 𝑦
41 vg 𝑔
42 38 cv 𝑥
43 42 22 cfv ( 2nd𝑥 )
44 40 cv 𝑦
45 43 44 34 co ( ( 2nd𝑥 ) 𝑦 )
46 vf 𝑓
47 42 34 cfv ( 𝑥 )
48 41 cv 𝑔
49 48 14 cfv ( 1st𝑔 )
50 42 14 cfv ( 1st𝑥 )
51 50 14 cfv ( 1st ‘ ( 1st𝑥 ) )
52 43 14 cfv ( 1st ‘ ( 2nd𝑥 ) )
53 51 52 cop ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩
54 5 36 cfv ( comp ‘ 𝑟 )
55 44 14 cfv ( 1st𝑦 )
56 53 55 54 co ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) )
57 46 cv 𝑓
58 57 14 cfv ( 1st𝑓 )
59 49 58 56 co ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) )
60 48 22 cfv ( 2nd𝑔 )
61 50 22 cfv ( 2nd ‘ ( 1st𝑥 ) )
62 43 22 cfv ( 2nd ‘ ( 2nd𝑥 ) )
63 61 62 cop ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩
64 7 36 cfv ( comp ‘ 𝑠 )
65 44 22 cfv ( 2nd𝑦 )
66 63 65 64 co ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) )
67 57 22 cfv ( 2nd𝑓 )
68 60 67 66 co ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) )
69 59 68 cop ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩
70 41 46 45 47 69 cmpo ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ )
71 38 40 39 12 70 cmpo ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) )
72 37 71 cop ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩
73 32 35 72 ctp { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ }
74 29 28 73 csb ( 𝑢𝑏 , 𝑣𝑏 ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) ) ) / { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ }
75 10 9 74 csb ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ( 𝑢𝑏 , 𝑣𝑏 ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) ) ) / { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ }
76 1 3 2 2 75 cmpo ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ( 𝑢𝑏 , 𝑣𝑏 ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) ) ) / { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } )
77 0 76 wceq ×c = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ( 𝑢𝑏 , 𝑣𝑏 ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝑟 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝑠 ) ( 2nd𝑣 ) ) ) ) / { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦𝑏 ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) 𝑦 ) , 𝑓 ∈ ( 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } )