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} ‘ 𝑓 ) ) ⟩ ) ) ⟩ } ) 