Step 
Hyp 
Ref 
Expression 
1 

xpcval.t 
⊢ 𝑇 = ( 𝐶 ×_{c} 𝐷 ) 
2 

xpcval.x 
⊢ 𝑋 = ( Base ‘ 𝐶 ) 
3 

xpcval.y 
⊢ 𝑌 = ( Base ‘ 𝐷 ) 
4 

xpcval.h 
⊢ 𝐻 = ( Hom ‘ 𝐶 ) 
5 

xpcval.j 
⊢ 𝐽 = ( Hom ‘ 𝐷 ) 
6 

xpcval.o1 
⊢ · = ( comp ‘ 𝐶 ) 
7 

xpcval.o2 
⊢ ∙ = ( comp ‘ 𝐷 ) 
8 

xpcval.c 
⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) 
9 

xpcval.d 
⊢ ( 𝜑 → 𝐷 ∈ 𝑊 ) 
10 

xpcval.b 
⊢ ( 𝜑 → 𝐵 = ( 𝑋 × 𝑌 ) ) 
11 

xpcval.k 
⊢ ( 𝜑 → 𝐾 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( ( ( 1^{st} ‘ 𝑢 ) 𝐻 ( 1^{st} ‘ 𝑣 ) ) × ( ( 2^{nd} ‘ 𝑢 ) 𝐽 ( 2^{nd} ‘ 𝑣 ) ) ) ) ) 
12 

xpcval.o 
⊢ ( 𝜑 → 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^{nd} ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^{st} ‘ 𝑔 ) ( ⟨ ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 1^{st} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ · ( 1^{st} ‘ 𝑦 ) ) ( 1^{st} ‘ 𝑓 ) ) , ( ( 2^{nd} ‘ 𝑔 ) ( ⟨ ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 2^{nd} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ∙ ( 2^{nd} ‘ 𝑦 ) ) ( 2^{nd} ‘ 𝑓 ) ) ⟩ ) ) ) 
13 

dfxpc 
⊢ ×_{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} ‘ 𝑓 ) ) ⟩ ) ) ⟩ } ) 
14 
13

a1i 
⊢ ( 𝜑 → ×_{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} ‘ 𝑓 ) ) ⟩ ) ) ⟩ } ) ) 
15 

fvex 
⊢ ( Base ‘ 𝑟 ) ∈ V 
16 

fvex 
⊢ ( Base ‘ 𝑠 ) ∈ V 
17 
15 16

xpex 
⊢ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) ∈ V 
18 
17

a1i 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) ∈ V ) 
19 

simprl 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → 𝑟 = 𝐶 ) 
20 
19

fveq2d 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝐶 ) ) 
21 
20 2

eqtr4di 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → ( Base ‘ 𝑟 ) = 𝑋 ) 
22 

simprr 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → 𝑠 = 𝐷 ) 
23 
22

fveq2d 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝐷 ) ) 
24 
23 3

eqtr4di 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → ( Base ‘ 𝑠 ) = 𝑌 ) 
25 
21 24

xpeq12d 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) = ( 𝑋 × 𝑌 ) ) 
26 
10

adantr 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → 𝐵 = ( 𝑋 × 𝑌 ) ) 
27 
25 26

eqtr4d 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) = 𝐵 ) 
28 

vex 
⊢ 𝑏 ∈ V 
29 
28 28

mpoex 
⊢ ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^{st} ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^{st} ‘ 𝑣 ) ) × ( ( 2^{nd} ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^{nd} ‘ 𝑣 ) ) ) ) ∈ V 
30 
29

a1i 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^{st} ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^{st} ‘ 𝑣 ) ) × ( ( 2^{nd} ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^{nd} ‘ 𝑣 ) ) ) ) ∈ V ) 
31 

simpr 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 ) 
32 

simplrl 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → 𝑟 = 𝐶 ) 
33 
32

fveq2d 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑟 ) = ( Hom ‘ 𝐶 ) ) 
34 
33 4

eqtr4di 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑟 ) = 𝐻 ) 
35 
34

oveqd 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( ( 1^{st} ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^{st} ‘ 𝑣 ) ) = ( ( 1^{st} ‘ 𝑢 ) 𝐻 ( 1^{st} ‘ 𝑣 ) ) ) 
36 

simplrr 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → 𝑠 = 𝐷 ) 
37 
36

fveq2d 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑠 ) = ( Hom ‘ 𝐷 ) ) 
38 
37 5

eqtr4di 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ 𝑠 ) = 𝐽 ) 
39 
38

oveqd 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( ( 2^{nd} ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^{nd} ‘ 𝑣 ) ) = ( ( 2^{nd} ‘ 𝑢 ) 𝐽 ( 2^{nd} ‘ 𝑣 ) ) ) 
40 
35 39

xpeq12d 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( ( ( 1^{st} ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^{st} ‘ 𝑣 ) ) × ( ( 2^{nd} ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^{nd} ‘ 𝑣 ) ) ) = ( ( ( 1^{st} ‘ 𝑢 ) 𝐻 ( 1^{st} ‘ 𝑣 ) ) × ( ( 2^{nd} ‘ 𝑢 ) 𝐽 ( 2^{nd} ‘ 𝑣 ) ) ) ) 
41 
31 31 40

mpoeq123dv 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^{st} ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^{st} ‘ 𝑣 ) ) × ( ( 2^{nd} ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^{nd} ‘ 𝑣 ) ) ) ) = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( ( ( 1^{st} ‘ 𝑢 ) 𝐻 ( 1^{st} ‘ 𝑣 ) ) × ( ( 2^{nd} ‘ 𝑢 ) 𝐽 ( 2^{nd} ‘ 𝑣 ) ) ) ) ) 
42 
11

ad2antrr 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → 𝐾 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( ( ( 1^{st} ‘ 𝑢 ) 𝐻 ( 1^{st} ‘ 𝑣 ) ) × ( ( 2^{nd} ‘ 𝑢 ) 𝐽 ( 2^{nd} ‘ 𝑣 ) ) ) ) ) 
43 
41 42

eqtr4d 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 1^{st} ‘ 𝑢 ) ( Hom ‘ 𝑟 ) ( 1^{st} ‘ 𝑣 ) ) × ( ( 2^{nd} ‘ 𝑢 ) ( Hom ‘ 𝑠 ) ( 2^{nd} ‘ 𝑣 ) ) ) ) = 𝐾 ) 
44 

simplr 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → 𝑏 = 𝐵 ) 
45 
44

opeq2d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ ) 
46 

simpr 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ℎ = 𝐾 ) 
47 
46

opeq2d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ⟨ ( Hom ‘ ndx ) , ℎ ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ ) 
48 
44 44

xpeq12d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) ) 
49 
46

oveqd 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( ( 2^{nd} ‘ 𝑥 ) ℎ 𝑦 ) = ( ( 2^{nd} ‘ 𝑥 ) 𝐾 𝑦 ) ) 
50 
46

fveq1d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( ℎ ‘ 𝑥 ) = ( 𝐾 ‘ 𝑥 ) ) 
51 
32

adantr 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → 𝑟 = 𝐶 ) 
52 
51

fveq2d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( comp ‘ 𝑟 ) = ( comp ‘ 𝐶 ) ) 
53 
52 6

eqtr4di 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( comp ‘ 𝑟 ) = · ) 
54 
53

oveqd 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( ⟨ ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 1^{st} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^{st} ‘ 𝑦 ) ) = ( ⟨ ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 1^{st} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ · ( 1^{st} ‘ 𝑦 ) ) ) 
55 
54

oveqd 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( ( 1^{st} ‘ 𝑔 ) ( ⟨ ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 1^{st} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑟 ) ( 1^{st} ‘ 𝑦 ) ) ( 1^{st} ‘ 𝑓 ) ) = ( ( 1^{st} ‘ 𝑔 ) ( ⟨ ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 1^{st} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ · ( 1^{st} ‘ 𝑦 ) ) ( 1^{st} ‘ 𝑓 ) ) ) 
56 
36

adantr 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → 𝑠 = 𝐷 ) 
57 
56

fveq2d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( comp ‘ 𝑠 ) = ( comp ‘ 𝐷 ) ) 
58 
57 7

eqtr4di 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( comp ‘ 𝑠 ) = ∙ ) 
59 
58

oveqd 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( ⟨ ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 2^{nd} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^{nd} ‘ 𝑦 ) ) = ( ⟨ ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 2^{nd} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ∙ ( 2^{nd} ‘ 𝑦 ) ) ) 
60 
59

oveqd 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( ( 2^{nd} ‘ 𝑔 ) ( ⟨ ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 2^{nd} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑠 ) ( 2^{nd} ‘ 𝑦 ) ) ( 2^{nd} ‘ 𝑓 ) ) = ( ( 2^{nd} ‘ 𝑔 ) ( ⟨ ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 2^{nd} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ∙ ( 2^{nd} ‘ 𝑦 ) ) ( 2^{nd} ‘ 𝑓 ) ) ) 
61 
55 60

opeq12d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ⟨ ( ( 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} ‘ 𝑓 ) ) ⟩ = ⟨ ( ( 1^{st} ‘ 𝑔 ) ( ⟨ ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 1^{st} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ · ( 1^{st} ‘ 𝑦 ) ) ( 1^{st} ‘ 𝑓 ) ) , ( ( 2^{nd} ‘ 𝑔 ) ( ⟨ ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 2^{nd} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ∙ ( 2^{nd} ‘ 𝑦 ) ) ( 2^{nd} ‘ 𝑓 ) ) ⟩ ) 
62 
49 50 61

mpoeq123dv 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( 𝑔 ∈ ( ( 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} ‘ 𝑓 ) ) ⟩ ) = ( 𝑔 ∈ ( ( 2^{nd} ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^{st} ‘ 𝑔 ) ( ⟨ ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 1^{st} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ · ( 1^{st} ‘ 𝑦 ) ) ( 1^{st} ‘ 𝑓 ) ) , ( ( 2^{nd} ‘ 𝑔 ) ( ⟨ ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 2^{nd} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ∙ ( 2^{nd} ‘ 𝑦 ) ) ( 2^{nd} ‘ 𝑓 ) ) ⟩ ) ) 
63 
48 44 62

mpoeq123dv 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 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} ‘ 𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^{nd} ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^{st} ‘ 𝑔 ) ( ⟨ ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 1^{st} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ · ( 1^{st} ‘ 𝑦 ) ) ( 1^{st} ‘ 𝑓 ) ) , ( ( 2^{nd} ‘ 𝑔 ) ( ⟨ ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 2^{nd} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ∙ ( 2^{nd} ‘ 𝑦 ) ) ( 2^{nd} ‘ 𝑓 ) ) ⟩ ) ) ) 
64 
12

ad3antrrr 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^{nd} ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^{st} ‘ 𝑔 ) ( ⟨ ( 1^{st} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 1^{st} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ · ( 1^{st} ‘ 𝑦 ) ) ( 1^{st} ‘ 𝑓 ) ) , ( ( 2^{nd} ‘ 𝑔 ) ( ⟨ ( 2^{nd} ‘ ( 1^{st} ‘ 𝑥 ) ) , ( 2^{nd} ‘ ( 2^{nd} ‘ 𝑥 ) ) ⟩ ∙ ( 2^{nd} ‘ 𝑦 ) ) ( 2^{nd} ‘ 𝑓 ) ) ⟩ ) ) ) 
65 
63 64

eqtr4d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ( 𝑥 ∈ ( 𝑏 × 𝑏 ) , 𝑦 ∈ 𝑏 ↦ ( 𝑔 ∈ ( ( 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} ‘ 𝑓 ) ) ⟩ ) ) = 𝑂 ) 
66 
65

opeq2d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → ⟨ ( 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} ‘ 𝑓 ) ) ⟩ ) ) ⟩ = ⟨ ( comp ‘ ndx ) , 𝑂 ⟩ ) 
67 
45 47 66

tpeq123d 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) ∧ ℎ = 𝐾 ) → { ⟨ ( 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} ‘ 𝑓 ) ) ⟩ ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , 𝑂 ⟩ } ) 
68 
30 43 67

csbied2 
⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) ∧ 𝑏 = 𝐵 ) → ⦋ ( 𝑢 ∈ 𝑏 , 𝑣 ∈ 𝑏 ↦ ( ( ( 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} ‘ 𝑓 ) ) ⟩ ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , 𝑂 ⟩ } ) 
69 
18 27 68

csbied2 
⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝐶 ∧ 𝑠 = 𝐷 ) ) → ⦋ ( ( 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} ‘ 𝑓 ) ) ⟩ ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , 𝑂 ⟩ } ) 
70 
8

elexd 
⊢ ( 𝜑 → 𝐶 ∈ V ) 
71 
9

elexd 
⊢ ( 𝜑 → 𝐷 ∈ V ) 
72 

tpex 
⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , 𝑂 ⟩ } ∈ V 
73 
72

a1i 
⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , 𝑂 ⟩ } ∈ V ) 
74 
14 69 70 71 73

ovmpod 
⊢ ( 𝜑 → ( 𝐶 ×_{c} 𝐷 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , 𝑂 ⟩ } ) 
75 
1 74

syl5eq 
⊢ ( 𝜑 → 𝑇 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , 𝑂 ⟩ } ) 