xpcbas

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

	Ref	Expression
Hypotheses	xpcbas.t	$⊢ T = C \times_{c} D$
	xpcbas.x	$⊢ X = {Base}_{C}$
	xpcbas.y	$⊢ Y = {Base}_{D}$
Assertion	xpcbas	$⊢ X \times Y = {Base}_{T}$

Proof

Step	Hyp	Ref	Expression
1		xpcbas.t	$⊢ T = C \times_{c} D$
2		xpcbas.x	$⊢ X = {Base}_{C}$
3		xpcbas.y	$⊢ Y = {Base}_{D}$
4		eqid	$⊢ Hom (C) = Hom (C)$
5		eqid	$⊢ Hom (D) = Hom (D)$
6		eqid	$⊢ comp (C) = comp (C)$
7		eqid	$⊢ comp (D) = comp (D)$
8		simpl	$⊢ (C \in V \land D \in V) \to C \in V$
9		simpr	$⊢ (C \in V \land D \in V) \to D \in V$
10		eqidd	$⊢ (C \in V \land D \in V) \to X \times Y = X \times Y$
11		eqidd	$⊢ (C \in V \land D \in V) \to (u \in (X \times Y), v \in (X \times Y) ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v))) = (u \in (X \times Y), v \in (X \times Y) ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v)))$
12		eqidd	$⊢ (C \in V \land D \in V) \to (x \in ((X \times Y) \times (X \times Y)), y \in (X \times Y) ⟼ (g \in (2^{nd} (x) (u \in (X \times Y), v \in (X \times Y) ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v))) y), f \in (u \in (X \times Y), v \in (X \times Y) ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 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 ((X \times Y) \times (X \times Y)), y \in (X \times Y) ⟼ (g \in (2^{nd} (x) (u \in (X \times Y), v \in (X \times Y) ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v))) y), f \in (u \in (X \times Y), v \in (X \times Y) ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 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)⟩))$
13	1 2 3 4 5 6 7 8 9 10 11 12	xpcval	$⊢ (C \in V \land D \in V) \to T = \{⟨{Base}_{ndx}, X \times Y⟩, ⟨Hom (ndx), (u \in (X \times Y), v \in (X \times Y) ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v)))⟩, ⟨comp (ndx), (x \in ((X \times Y) \times (X \times Y)), y \in (X \times Y) ⟼ (g \in (2^{nd} (x) (u \in (X \times Y), v \in (X \times Y) ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v))) y), f \in (u \in (X \times Y), v \in (X \times Y) ⟼ (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 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)⟩))⟩\}$
14	2	fvexi	$⊢ X \in V$
15	3	fvexi	$⊢ Y \in V$
16	14 15	xpex	$⊢ X \times Y \in V$
17	16	a1i	$⊢ (C \in V \land D \in V) \to X \times Y \in V$
18	13 17	estrreslem1	$⊢ (C \in V \land D \in V) \to X \times Y = {Base}_{T}$
19		base0	$⊢ \emptyset = {Base}_{\emptyset}$
20		fvprc	$⊢ \neg C \in V \to {Base}_{C} = \emptyset$
21	2 20	eqtrid	$⊢ \neg C \in V \to X = \emptyset$
22		fvprc	$⊢ \neg D \in V \to {Base}_{D} = \emptyset$
23	3 22	eqtrid	$⊢ \neg D \in V \to Y = \emptyset$
24	21 23	orim12i	$⊢ (\neg C \in V \lor \neg D \in V) \to (X = \emptyset \lor Y = \emptyset)$
25		ianor	$⊢ \neg (C \in V \land D \in V) \leftrightarrow (\neg C \in V \lor \neg D \in V)$
26		xpeq0	$⊢ X \times Y = \emptyset \leftrightarrow (X = \emptyset \lor Y = \emptyset)$
27	24 25 26	3imtr4i	$⊢ \neg (C \in V \land D \in V) \to X \times Y = \emptyset$
28		fnxpc	$⊢ \times_{c} Fn (V \times V)$
29		fndm	$⊢ \times_{c} Fn (V \times V) \to dom \times_{c} = V \times V$
30	28 29	ax-mp	$⊢ dom \times_{c} = V \times V$
31	30	ndmov	$⊢ \neg (C \in V \land D \in V) \to C \times_{c} D = \emptyset$
32	1 31	eqtrid	$⊢ \neg (C \in V \land D \in V) \to T = \emptyset$
33	32	fveq2d	$⊢ \neg (C \in V \land D \in V) \to {Base}_{T} = {Base}_{\emptyset}$
34	19 27 33	3eqtr4a	$⊢ \neg (C \in V \land D \in V) \to X \times Y = {Base}_{T}$
35	18 34	pm2.61i	$⊢ X \times Y = {Base}_{T}$

Metamath Proof Explorer

Theorem xpcbas

Proof