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 ‘ 𝑠 ) ) / 𝑏 ⦌ ⦋ ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^nd ‘ 𝑣 ) ) ) ) / ℎ ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } )

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	⊢ 1^st
15	11	cv	⊢ 𝑢
16	15 14	cfv	⊢ ( 1^st ‘ 𝑢 )
17		chom	⊢ Hom
18	5 17	cfv	⊢ ( Hom ‘ 𝑟 )
19	13	cv	⊢ 𝑣
20	19 14	cfv	⊢ ( 1^st ‘ 𝑣 )
21	16 20 18	co	⊢ ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^st ‘ 𝑣 ) )
22		c2nd	⊢ 2^nd
23	15 22	cfv	⊢ ( 2^nd ‘ 𝑢 )
24	7 17	cfv	⊢ ( Hom ‘ 𝑠 )
25	19 22	cfv	⊢ ( 2^nd ‘ 𝑣 )
26	23 25 24	co	⊢ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^nd ‘ 𝑣 ) )
27	21 26	cxp	⊢ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^nd ‘ 𝑣 ) ) )
28	11 13 12 12 27	cmpo	⊢ ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^nd ‘ 𝑣 ) ) ) )
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	⊢ ( 2^nd ‘ 𝑥 )
44	40	cv	⊢ 𝑦
45	43 44 34	co	⊢ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 )
46		vf	⊢ 𝑓
47	42 34	cfv	⊢ ( ℎ ‘ 𝑥 )
48	41	cv	⊢ 𝑔
49	48 14	cfv	⊢ ( 1^st ‘ 𝑔 )
50	42 14	cfv	⊢ ( 1^st ‘ 𝑥 )
51	50 14	cfv	⊢ ( 1^st ‘ ( 1^st ‘ 𝑥 ) )
52	43 14	cfv	⊢ ( 1^st ‘ ( 2^nd ‘ 𝑥 ) )
53	51 52	cop	⊢ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩
54	5 36	cfv	⊢ ( comp ‘ 𝑟 )
55	44 14	cfv	⊢ ( 1^st ‘ 𝑦 )
56	53 55 54	co	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) )
57	46	cv	⊢ 𝑓
58	57 14	cfv	⊢ ( 1^st ‘ 𝑓 )
59	49 58 56	co	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) )
60	48 22	cfv	⊢ ( 2^nd ‘ 𝑔 )
61	50 22	cfv	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) )
62	43 22	cfv	⊢ ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) )
63	61 62	cop	⊢ ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩
64	7 36	cfv	⊢ ( comp ‘ 𝑠 )
65	44 22	cfv	⊢ ( 2^nd ‘ 𝑦 )
66	63 65 64	co	⊢ ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) )
67	57 22	cfv	⊢ ( 2^nd ‘ 𝑓 )
68	60 67 66	co	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) )
69	59 68	cop	⊢ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩
70	41 46 45 47 69	cmpo	⊢ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
71	38 40 39 12 70	cmpo	⊢ ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
72	37 71	cop	⊢ ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩
73	32 35 72	ctp	⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ }
74	29 28 73	csb	⊢ ⦋ ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^nd ‘ 𝑣 ) ) ) ) / ℎ ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ }
75	10 9 74	csb	⊢ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ ⦋ ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^nd ‘ 𝑣 ) ) ) ) / ℎ ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ }
76	1 3 2 2 75	cmpo	⊢ ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ ⦋ ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^nd ‘ 𝑣 ) ) ) ) / ℎ ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } )
77	0 76	wceq	⊢ ×_c = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ ⦋ ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^nd ‘ 𝑣 ) ) ) ) / ℎ ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ℎ 𝑦 ) , 𝑓 ∈ ( ℎ ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } )

Metamath Proof Explorer

Definition df-xpc

Detailed syntax breakdown