xpccofval

Description: Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017) (Proof shortened by AV, 2-Mar-2024)

	Ref	Expression
Hypotheses	xpccofval.t	$⊢ T = C \times_{c} D$
	xpccofval.b	$⊢ B = {Base}_{T}$
	xpccofval.k	$⊢ K = Hom (T)$
	xpccofval.o1	$⊢ \underset{˙}{\cdot} = comp (C)$
	xpccofval.o2	$⊢ \underset{˙}{∙} = comp (D)$
	xpccofval.o	$⊢ O = comp (T)$
Assertion	xpccofval	$⊢ 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)⟩))$

Proof

Step	Hyp	Ref	Expression
1		xpccofval.t	$⊢ T = C \times_{c} D$
2		xpccofval.b	$⊢ B = {Base}_{T}$
3		xpccofval.k	$⊢ K = Hom (T)$
4		xpccofval.o1	$⊢ \underset{˙}{\cdot} = comp (C)$
5		xpccofval.o2	$⊢ \underset{˙}{∙} = comp (D)$
6		xpccofval.o	$⊢ O = comp (T)$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8		eqid	$⊢ {Base}_{D} = {Base}_{D}$
9		eqid	$⊢ Hom (C) = Hom (C)$
10		eqid	$⊢ Hom (D) = Hom (D)$
11		simpl	$⊢ (C \in V \land D \in V) \to C \in V$
12		simpr	$⊢ (C \in V \land D \in V) \to D \in V$
13	1 7 8	xpcbas	$⊢ {Base}_{C} \times {Base}_{D} = {Base}_{T}$
14	2 13	eqtr4i	$⊢ B = {Base}_{C} \times {Base}_{D}$
15	14	a1i	$⊢ (C \in V \land D \in V) \to B = {Base}_{C} \times {Base}_{D}$
16	1 2 9 10 3	xpchomfval	$⊢ K = (u \in B, v \in B ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v)))$
17	16	a1i	$⊢ (C \in V \land D \in V) \to K = (u \in B, v \in B ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v)))$
18		eqidd	$⊢ (C \in V \land D \in V) \to (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)⟩)) = (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)⟩))$
19	1 7 8 9 10 4 5 11 12 15 17 18	xpcval	$⊢ (C \in V \land D \in V) \to T = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), (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)⟩))⟩\}$
20		catstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), (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)⟩))⟩\} Struct ⟨1, 15⟩$
21		ccoid	$⊢ comp = Slot comp (ndx)$
22		snsstp3	$⊢ \{⟨comp (ndx), (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)⟩))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), K⟩, ⟨comp (ndx), (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)⟩))⟩\}$
23	2	fvexi	$⊢ B \in V$
24	23 23	xpex	$⊢ B \times B \in V$
25	24 23	mpoex	$⊢ (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)⟩)) \in V$
26	25	a1i	$⊢ (C \in V \land D \in V) \to (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)⟩)) \in V$
27	19 20 21 22 26 6	strfv3	$⊢ (C \in V \land D \in V) \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)⟩))$
28		fnxpc	$⊢ \times_{c} Fn (V \times V)$
29	28	fndmi	$⊢ dom \times_{c} = V \times V$
30	29	ndmov	$⊢ \neg (C \in V \land D \in V) \to C \times_{c} D = \emptyset$
31	1 30	eqtrid	$⊢ \neg (C \in V \land D \in V) \to T = \emptyset$
32	31	fveq2d	$⊢ \neg (C \in V \land D \in V) \to comp (T) = comp (\emptyset)$
33	21	str0	$⊢ \emptyset = comp (\emptyset)$
34	32 6 33	3eqtr4g	$⊢ \neg (C \in V \land D \in V) \to O = \emptyset$
35	31	fveq2d	$⊢ \neg (C \in V \land D \in V) \to {Base}_{T} = {Base}_{\emptyset}$
36		base0	$⊢ \emptyset = {Base}_{\emptyset}$
37	35 2 36	3eqtr4g	$⊢ \neg (C \in V \land D \in V) \to B = \emptyset$
38	37	olcd	$⊢ \neg (C \in V \land D \in V) \to (B \times B = \emptyset \lor B = \emptyset)$
39		0mpo0	$⊢ (B \times B = \emptyset \lor B = \emptyset) \to (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)⟩)) = \emptyset$
40	38 39	syl	$⊢ \neg (C \in V \land D \in V) \to (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)⟩)) = \emptyset$
41	34 40	eqtr4d	$⊢ \neg (C \in V \land D \in V) \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)⟩))$
42	27 41	pm2.61i	$⊢ 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)⟩))$

Metamath Proof Explorer

Theorem xpccofval

Proof