xpcval

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

	Ref	Expression
Hypotheses	xpcval.t	$⊢ T = C \times_{c} D$
	xpcval.x	$⊢ X = {Base}_{C}$
	xpcval.y	$⊢ Y = {Base}_{D}$
	xpcval.h	$⊢ H = Hom (C)$
	xpcval.j	$⊢ J = Hom (D)$
	xpcval.o1	$⊢ \underset{˙}{\cdot} = comp (C)$
	xpcval.o2	$⊢ \underset{˙}{∙} = comp (D)$
	xpcval.c	$⊢ φ \to C \in V$
	xpcval.d	$⊢ φ \to D \in W$
	xpcval.b	$⊢ φ \to B = X \times Y$
	xpcval.k	$⊢ φ \to K = (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))$
	xpcval.o	$⊢ φ \to O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩))$
Assertion	xpcval	$⊢ φ \to T = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), O⟩\}$

Proof

Step	Hyp	Ref	Expression
1		xpcval.t	$⊢ T = C \times_{c} D$
2		xpcval.x	$⊢ X = {Base}_{C}$
3		xpcval.y	$⊢ Y = {Base}_{D}$
4		xpcval.h	$⊢ H = Hom (C)$
5		xpcval.j	$⊢ J = Hom (D)$
6		xpcval.o1	$⊢ \underset{˙}{\cdot} = comp (C)$
7		xpcval.o2	$⊢ \underset{˙}{∙} = comp (D)$
8		xpcval.c	$⊢ φ \to C \in V$
9		xpcval.d	$⊢ φ \to D \in W$
10		xpcval.b	$⊢ φ \to B = X \times Y$
11		xpcval.k	$⊢ φ \to K = (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))$
12		xpcval.o	$⊢ φ \to O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩))$
13		df-xpc	$⊢ \times_{c} = (r \in V, s \in V ⟼ ⦋ ({Base}_{r} \times {Base}_{s}) / b ⦌ ⦋ (u \in b, v \in b ⟼ (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v))) / h ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), h⟩, ⟨comp (ndx), (x \in (b \times b), y \in b ⟼ (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\})$
14	13	a1i	$⊢ φ \to \times_{c} = (r \in V, s \in V ⟼ ⦋ ({Base}_{r} \times {Base}_{s}) / b ⦌ ⦋ (u \in b, v \in b ⟼ (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v))) / h ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), h⟩, ⟨comp (ndx), (x \in (b \times b), y \in b ⟼ (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\})$
15		fvex	$⊢ {Base}_{r} \in V$
16		fvex	$⊢ {Base}_{s} \in V$
17	15 16	xpex	$⊢ {Base}_{r} \times {Base}_{s} \in V$
18	17	a1i	$⊢ (φ \land (r = C \land s = D)) \to {Base}_{r} \times {Base}_{s} \in V$
19		simprl	$⊢ (φ \land (r = C \land s = D)) \to r = C$
20	19	fveq2d	$⊢ (φ \land (r = C \land s = D)) \to {Base}_{r} = {Base}_{C}$
21	20 2	eqtr4di	$⊢ (φ \land (r = C \land s = D)) \to {Base}_{r} = X$
22		simprr	$⊢ (φ \land (r = C \land s = D)) \to s = D$
23	22	fveq2d	$⊢ (φ \land (r = C \land s = D)) \to {Base}_{s} = {Base}_{D}$
24	23 3	eqtr4di	$⊢ (φ \land (r = C \land s = D)) \to {Base}_{s} = Y$
25	21 24	xpeq12d	$⊢ (φ \land (r = C \land s = D)) \to {Base}_{r} \times {Base}_{s} = X \times Y$
26	10	adantr	$⊢ (φ \land (r = C \land s = D)) \to B = X \times Y$
27	25 26	eqtr4d	$⊢ (φ \land (r = C \land s = D)) \to {Base}_{r} \times {Base}_{s} = B$
28		vex	$⊢ b \in V$
29	28 28	mpoex	$⊢ (u \in b, v \in b ⟼ (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v))) \in V$
30	29	a1i	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to (u \in b, v \in b ⟼ (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v))) \in V$
31		simpr	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to b = B$
32		simplrl	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to r = C$
33	32	fveq2d	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to Hom (r) = Hom (C)$
34	33 4	eqtr4di	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to Hom (r) = H$
35	34	oveqd	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to 1^{st} (u) Hom (r) 1^{st} (v) = 1^{st} (u) H 1^{st} (v)$
36		simplrr	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to s = D$
37	36	fveq2d	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to Hom (s) = Hom (D)$
38	37 5	eqtr4di	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to Hom (s) = J$
39	38	oveqd	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to 2^{nd} (u) Hom (s) 2^{nd} (v) = 2^{nd} (u) J 2^{nd} (v)$
40	35 39	xpeq12d	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v)) = (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))$
41	31 31 40	mpoeq123dv	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to (u \in b, v \in b ⟼ (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v))) = (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))$
42	11	ad2antrr	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to K = (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))$
43	41 42	eqtr4d	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to (u \in b, v \in b ⟼ (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v))) = K$
44		simplr	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to b = B$
45	44	opeq2d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to ⟨{Base}_{ndx}, b⟩ = ⟨{Base}_{ndx}, B⟩$
46		simpr	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to h = K$
47	46	opeq2d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to ⟨Hom (ndx), h⟩ = ⟨Hom (ndx), K⟩$
48	44 44	xpeq12d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to b \times b = B \times B$
49	46	oveqd	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to 2^{nd} (x) h y = 2^{nd} (x) K y$
50	46	fveq1d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to h (x) = K (x)$
51	32	adantr	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to r = C$
52	51	fveq2d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to comp (r) = comp (C)$
53	52 6	eqtr4di	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to comp (r) = \underset{˙}{\cdot}$
54	53	oveqd	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to ⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y) = ⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)$
55	54	oveqd	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f) = 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f)$
56	36	adantr	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to s = D$
57	56	fveq2d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to comp (s) = comp (D)$
58	57 7	eqtr4di	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to comp (s) = \underset{˙}{∙}$
59	58	oveqd	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to ⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y) = ⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)$
60	59	oveqd	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f) = 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)$
61	55 60	opeq12d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩ = ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩$
62	49 50 61	mpoeq123dv	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩) = (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩)$
63	48 44 62	mpoeq123dv	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to (x \in (b \times b), y \in b ⟼ (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩)) = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩))$
64	12	ad3antrrr	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩))$
65	63 64	eqtr4d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to (x \in (b \times b), y \in b ⟼ (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩)) = O$
66	65	opeq2d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to ⟨comp (ndx), (x \in (b \times b), y \in b ⟼ (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩))⟩ = ⟨comp (ndx), O⟩$
67	45 47 66	tpeq123d	$⊢ (((φ \land (r = C \land s = D)) \land b = B) \land h = K) \to \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), h⟩, ⟨comp (ndx), (x \in (b \times b), y \in b ⟼ (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), O⟩\}$
68	30 43 67	csbied2	$⊢ ((φ \land (r = C \land s = D)) \land b = B) \to ⦋ (u \in b, v \in b ⟼ (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v))) / h ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), h⟩, ⟨comp (ndx), (x \in (b \times b), y \in b ⟼ (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), O⟩\}$
69	18 27 68	csbied2	$⊢ (φ \land (r = C \land s = D)) \to ⦋ ({Base}_{r} \times {Base}_{s}) / b ⦌ ⦋ (u \in b, v \in b ⟼ (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v))) / h ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), h⟩, ⟨comp (ndx), (x \in (b \times b), y \in b ⟼ (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), O⟩\}$
70	8	elexd	$⊢ φ \to C \in V$
71	9	elexd	$⊢ φ \to D \in V$
72		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), O⟩\} \in V$
73	72	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), O⟩\} \in V$
74	14 69 70 71 73	ovmpod	$⊢ φ \to C \times_{c} D = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), O⟩\}$
75	1 74	syl5eq	$⊢ φ \to T = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), O⟩\}$

Metamath Proof Explorer

Theorem xpcval

Proof