xpcval

Description: Value of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017)

	Ref	Expression
Hypotheses	xpcval.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
	xpcval.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
	xpcval.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
	xpcval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	xpcval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	xpcval.o1	⊢ · = ( comp ‘ 𝐶 )
	xpcval.o2	⊢ ∙ = ( comp ‘ 𝐷 )
	xpcval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	xpcval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
	xpcval.b	⊢ ( 𝜑 → 𝐵 = ( 𝑋 × 𝑌 ) )
	xpcval.k	⊢ ( 𝜑 → 𝐾 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( ( ( 1^st ‘ 𝑢 ) 𝐻 ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) 𝐽 ( 2^nd ‘ 𝑣 ) ) ) ) )
	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 ‘ 𝑓 ) ) ⟩ ) ) )
Assertion	xpcval	⊢ ( 𝜑 → 𝑇 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , 𝑂 ⟩ } )

Proof

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

Metamath Proof Explorer

Theorem xpcval

Proof