xpchomfval

Description: Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

	Ref	Expression
Hypotheses	xpchomfval.t	$⊢ T = C \times_{c} D$
	xpchomfval.y	$⊢ B = {Base}_{T}$
	xpchomfval.h	$⊢ H = Hom (C)$
	xpchomfval.j	$⊢ J = Hom (D)$
	xpchomfval.k	$⊢ K = Hom (T)$
Assertion	xpchomfval	$⊢ K = (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))$

Proof

Step	Hyp	Ref	Expression
1		xpchomfval.t	$⊢ T = C \times_{c} D$
2		xpchomfval.y	$⊢ B = {Base}_{T}$
3		xpchomfval.h	$⊢ H = Hom (C)$
4		xpchomfval.j	$⊢ J = Hom (D)$
5		xpchomfval.k	$⊢ K = Hom (T)$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7		eqid	$⊢ {Base}_{D} = {Base}_{D}$
8		eqid	$⊢ comp (C) = comp (C)$
9		eqid	$⊢ comp (D) = comp (D)$
10		simpl	$⊢ (C \in V \land D \in V) \to C \in V$
11		simpr	$⊢ (C \in V \land D \in V) \to D \in V$
12	1 6 7	xpcbas	$⊢ {Base}_{C} \times {Base}_{D} = {Base}_{T}$
13	2 12	eqtr4i	$⊢ B = {Base}_{C} \times {Base}_{D}$
14	13	a1i	$⊢ (C \in V \land D \in V) \to B = {Base}_{C} \times {Base}_{D}$
15		eqidd	$⊢ (C \in V \land D \in V) \to (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) = (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))$
16		eqidd	$⊢ (C \in V \land D \in V) \to (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) y), f \in (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (C) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (D) 2^{nd} (y)) 2^{nd} (f)⟩)) = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) y), f \in (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (C) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (D) 2^{nd} (y)) 2^{nd} (f)⟩))$
17	1 6 7 3 4 8 9 10 11 14 15 16	xpcval	$⊢ (C \in V \land D \in V) \to T = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))⟩, ⟨comp (ndx), (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) y), f \in (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (C) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (D) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\}$
18		catstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))⟩, ⟨comp (ndx), (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) y), f \in (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (C) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (D) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\} Struct ⟨1, 15⟩$
19		homid	$⊢ Hom = Slot Hom (ndx)$
20		snsstp2	$⊢ \{⟨Hom (ndx), (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))⟩, ⟨comp (ndx), (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) y), f \in (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (C) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (D) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\}$
21	2	fvexi	$⊢ B \in V$
22	21 21	mpoex	$⊢ (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) \in V$
23	22	a1i	$⊢ (C \in V \land D \in V) \to (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) \in V$
24	17 18 19 20 23 5	strfv3	$⊢ (C \in V \land D \in V) \to K = (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))$
25		fnxpc	$⊢ \times_{c} Fn (V \times V)$
26		fndm	$⊢ \times_{c} Fn (V \times V) \to dom \times_{c} = V \times V$
27	25 26	ax-mp	$⊢ dom \times_{c} = V \times V$
28	27	ndmov	$⊢ \neg (C \in V \land D \in V) \to C \times_{c} D = \emptyset$
29	1 28	syl5eq	$⊢ \neg (C \in V \land D \in V) \to T = \emptyset$
30	29	fveq2d	$⊢ \neg (C \in V \land D \in V) \to Hom (T) = Hom (\emptyset)$
31	19	str0	$⊢ \emptyset = Hom (\emptyset)$
32	30 5 31	3eqtr4g	$⊢ \neg (C \in V \land D \in V) \to K = \emptyset$
33	29	fveq2d	$⊢ \neg (C \in V \land D \in V) \to {Base}_{T} = {Base}_{\emptyset}$
34		base0	$⊢ \emptyset = {Base}_{\emptyset}$
35	33 2 34	3eqtr4g	$⊢ \neg (C \in V \land D \in V) \to B = \emptyset$
36	35	olcd	$⊢ \neg (C \in V \land D \in V) \to (B = \emptyset \lor B = \emptyset)$
37		0mpo0	$⊢ (B = \emptyset \lor B = \emptyset) \to (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) = \emptyset$
38	36 37	syl	$⊢ \neg (C \in V \land D \in V) \to (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v))) = \emptyset$
39	32 38	eqtr4d	$⊢ \neg (C \in V \land D \in V) \to K = (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))$
40	24 39	pm2.61i	$⊢ K = (u \in B, v \in B ⟼ (1^{st} (u) H 1^{st} (v)) \times (2^{nd} (u) J 2^{nd} (v)))$

Metamath Proof Explorer

Theorem xpchomfval

Proof