xpcpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same product category. (Contributed by Mario Carneiro, 17-Jan-2017)

	Ref	Expression
Hypotheses	xpcpropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
	xpcpropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
	xpcpropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	xpcpropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
	xpcpropd.a	$⊢ φ \to A \in V$
	xpcpropd.b	$⊢ φ \to B \in V$
	xpcpropd.c	$⊢ φ \to C \in V$
	xpcpropd.d	$⊢ φ \to D \in V$
Assertion	xpcpropd	$⊢ φ \to A \times_{c} C = B \times_{c} D$

Proof

Step	Hyp	Ref	Expression
1		xpcpropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
2		xpcpropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
3		xpcpropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
4		xpcpropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
5		xpcpropd.a	$⊢ φ \to A \in V$
6		xpcpropd.b	$⊢ φ \to B \in V$
7		xpcpropd.c	$⊢ φ \to C \in V$
8		xpcpropd.d	$⊢ φ \to D \in V$
9		eqid	$⊢ A \times_{c} C = A \times_{c} C$
10		eqid	$⊢ {Base}_{A} = {Base}_{A}$
11		eqid	$⊢ {Base}_{C} = {Base}_{C}$
12		eqid	$⊢ Hom (A) = Hom (A)$
13		eqid	$⊢ Hom (C) = Hom (C)$
14		eqid	$⊢ comp (A) = comp (A)$
15		eqid	$⊢ comp (C) = comp (C)$
16		eqidd	$⊢ φ \to {Base}_{A} \times {Base}_{C} = {Base}_{A} \times {Base}_{C}$
17	9 10 11	xpcbas	$⊢ {Base}_{A} \times {Base}_{C} = {Base}_{(A \times_{c} C)}$
18		eqid	$⊢ Hom (A \times_{c} C) = Hom (A \times_{c} C)$
19	9 17 12 13 18	xpchomfval	$⊢ Hom (A \times_{c} C) = (u \in ({Base}_{A} \times {Base}_{C}), v \in ({Base}_{A} \times {Base}_{C}) ⟼ (1^{st} (u) Hom (A) 1^{st} (v)) \times (2^{nd} (u) Hom (C) 2^{nd} (v)))$
20	19	a1i	$⊢ φ \to Hom (A \times_{c} C) = (u \in ({Base}_{A} \times {Base}_{C}), v \in ({Base}_{A} \times {Base}_{C}) ⟼ (1^{st} (u) Hom (A) 1^{st} (v)) \times (2^{nd} (u) Hom (C) 2^{nd} (v)))$
21		eqidd	$⊢ φ \to (x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})), y \in ({Base}_{A} \times {Base}_{C}) ⟼ (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f)⟩)) = (x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})), y \in ({Base}_{A} \times {Base}_{C}) ⟼ (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f)⟩))$
22	9 10 11 12 13 14 15 5 7 16 20 21	xpcval	$⊢ φ \to A \times_{c} C = \{⟨{Base}_{ndx}, {Base}_{A} \times {Base}_{C}⟩, ⟨Hom (ndx), Hom (A \times_{c} C)⟩, ⟨comp (ndx), (x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})), y \in ({Base}_{A} \times {Base}_{C}) ⟼ (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\}$
23		eqid	$⊢ B \times_{c} D = B \times_{c} D$
24		eqid	$⊢ {Base}_{B} = {Base}_{B}$
25		eqid	$⊢ {Base}_{D} = {Base}_{D}$
26		eqid	$⊢ Hom (B) = Hom (B)$
27		eqid	$⊢ Hom (D) = Hom (D)$
28		eqid	$⊢ comp (B) = comp (B)$
29		eqid	$⊢ comp (D) = comp (D)$
30	1	homfeqbas	$⊢ φ \to {Base}_{A} = {Base}_{B}$
31	3	homfeqbas	$⊢ φ \to {Base}_{C} = {Base}_{D}$
32	30 31	xpeq12d	$⊢ φ \to {Base}_{A} \times {Base}_{C} = {Base}_{B} \times {Base}_{D}$
33	1	3ad2ant1	$⊢ (φ \land u \in ({Base}_{A} \times {Base}_{C}) \land v \in ({Base}_{A} \times {Base}_{C})) \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
34		xp1st	$⊢ u \in ({Base}_{A} \times {Base}_{C}) \to 1^{st} (u) \in {Base}_{A}$
35	34	3ad2ant2	$⊢ (φ \land u \in ({Base}_{A} \times {Base}_{C}) \land v \in ({Base}_{A} \times {Base}_{C})) \to 1^{st} (u) \in {Base}_{A}$
36		xp1st	$⊢ v \in ({Base}_{A} \times {Base}_{C}) \to 1^{st} (v) \in {Base}_{A}$
37	36	3ad2ant3	$⊢ (φ \land u \in ({Base}_{A} \times {Base}_{C}) \land v \in ({Base}_{A} \times {Base}_{C})) \to 1^{st} (v) \in {Base}_{A}$
38	10 12 26 33 35 37	homfeqval	$⊢ (φ \land u \in ({Base}_{A} \times {Base}_{C}) \land v \in ({Base}_{A} \times {Base}_{C})) \to 1^{st} (u) Hom (A) 1^{st} (v) = 1^{st} (u) Hom (B) 1^{st} (v)$
39	3	3ad2ant1	$⊢ (φ \land u \in ({Base}_{A} \times {Base}_{C}) \land v \in ({Base}_{A} \times {Base}_{C})) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
40		xp2nd	$⊢ u \in ({Base}_{A} \times {Base}_{C}) \to 2^{nd} (u) \in {Base}_{C}$
41	40	3ad2ant2	$⊢ (φ \land u \in ({Base}_{A} \times {Base}_{C}) \land v \in ({Base}_{A} \times {Base}_{C})) \to 2^{nd} (u) \in {Base}_{C}$
42		xp2nd	$⊢ v \in ({Base}_{A} \times {Base}_{C}) \to 2^{nd} (v) \in {Base}_{C}$
43	42	3ad2ant3	$⊢ (φ \land u \in ({Base}_{A} \times {Base}_{C}) \land v \in ({Base}_{A} \times {Base}_{C})) \to 2^{nd} (v) \in {Base}_{C}$
44	11 13 27 39 41 43	homfeqval	$⊢ (φ \land u \in ({Base}_{A} \times {Base}_{C}) \land v \in ({Base}_{A} \times {Base}_{C})) \to 2^{nd} (u) Hom (C) 2^{nd} (v) = 2^{nd} (u) Hom (D) 2^{nd} (v)$
45	38 44	xpeq12d	$⊢ (φ \land u \in ({Base}_{A} \times {Base}_{C}) \land v \in ({Base}_{A} \times {Base}_{C})) \to (1^{st} (u) Hom (A) 1^{st} (v)) \times (2^{nd} (u) Hom (C) 2^{nd} (v)) = (1^{st} (u) Hom (B) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v))$
46	45	mpoeq3dva	$⊢ φ \to (u \in ({Base}_{A} \times {Base}_{C}), v \in ({Base}_{A} \times {Base}_{C}) ⟼ (1^{st} (u) Hom (A) 1^{st} (v)) \times (2^{nd} (u) Hom (C) 2^{nd} (v))) = (u \in ({Base}_{A} \times {Base}_{C}), v \in ({Base}_{A} \times {Base}_{C}) ⟼ (1^{st} (u) Hom (B) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v)))$
47	19 46	syl5eq	$⊢ φ \to Hom (A \times_{c} C) = (u \in ({Base}_{A} \times {Base}_{C}), v \in ({Base}_{A} \times {Base}_{C}) ⟼ (1^{st} (u) Hom (B) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v)))$
48	1	ad4antr	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
49	2	ad4antr	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
50		simp-4r	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))$
51		xp1st	$⊢ x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})) \to 1^{st} (x) \in ({Base}_{A} \times {Base}_{C})$
52	50 51	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 1^{st} (x) \in ({Base}_{A} \times {Base}_{C})$
53		xp1st	$⊢ 1^{st} (x) \in ({Base}_{A} \times {Base}_{C}) \to 1^{st} (1^{st} (x)) \in {Base}_{A}$
54	52 53	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 1^{st} (1^{st} (x)) \in {Base}_{A}$
55		xp2nd	$⊢ x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})) \to 2^{nd} (x) \in ({Base}_{A} \times {Base}_{C})$
56	50 55	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 2^{nd} (x) \in ({Base}_{A} \times {Base}_{C})$
57		xp1st	$⊢ 2^{nd} (x) \in ({Base}_{A} \times {Base}_{C}) \to 1^{st} (2^{nd} (x)) \in {Base}_{A}$
58	56 57	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 1^{st} (2^{nd} (x)) \in {Base}_{A}$
59		simpllr	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to y \in ({Base}_{A} \times {Base}_{C})$
60		xp1st	$⊢ y \in ({Base}_{A} \times {Base}_{C}) \to 1^{st} (y) \in {Base}_{A}$
61	59 60	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 1^{st} (y) \in {Base}_{A}$
62		simpr	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to f \in Hom (A \times_{c} C) (x)$
63		1st2nd2	$⊢ x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
64	50 63	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
65	64	fveq2d	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to Hom (A \times_{c} C) (x) = Hom (A \times_{c} C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
66		df-ov	$⊢ 1^{st} (x) Hom (A \times_{c} C) 2^{nd} (x) = Hom (A \times_{c} C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
67	65 66	eqtr4di	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to Hom (A \times_{c} C) (x) = 1^{st} (x) Hom (A \times_{c} C) 2^{nd} (x)$
68	9 17 12 13 18 52 56	xpchom	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 1^{st} (x) Hom (A \times_{c} C) 2^{nd} (x) = (1^{st} (1^{st} (x)) Hom (A) 1^{st} (2^{nd} (x))) \times (2^{nd} (1^{st} (x)) Hom (C) 2^{nd} (2^{nd} (x)))$
69	67 68	eqtrd	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to Hom (A \times_{c} C) (x) = (1^{st} (1^{st} (x)) Hom (A) 1^{st} (2^{nd} (x))) \times (2^{nd} (1^{st} (x)) Hom (C) 2^{nd} (2^{nd} (x)))$
70	62 69	eleqtrd	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to f \in ((1^{st} (1^{st} (x)) Hom (A) 1^{st} (2^{nd} (x))) \times (2^{nd} (1^{st} (x)) Hom (C) 2^{nd} (2^{nd} (x))))$
71		xp1st	$⊢ f \in ((1^{st} (1^{st} (x)) Hom (A) 1^{st} (2^{nd} (x))) \times (2^{nd} (1^{st} (x)) Hom (C) 2^{nd} (2^{nd} (x)))) \to 1^{st} (f) \in (1^{st} (1^{st} (x)) Hom (A) 1^{st} (2^{nd} (x)))$
72	70 71	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 1^{st} (f) \in (1^{st} (1^{st} (x)) Hom (A) 1^{st} (2^{nd} (x)))$
73		simplr	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to g \in (2^{nd} (x) Hom (A \times_{c} C) y)$
74	9 17 12 13 18 56 59	xpchom	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 2^{nd} (x) Hom (A \times_{c} C) y = (1^{st} (2^{nd} (x)) Hom (A) 1^{st} (y)) \times (2^{nd} (2^{nd} (x)) Hom (C) 2^{nd} (y))$
75	73 74	eleqtrd	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to g \in ((1^{st} (2^{nd} (x)) Hom (A) 1^{st} (y)) \times (2^{nd} (2^{nd} (x)) Hom (C) 2^{nd} (y)))$
76		xp1st	$⊢ g \in ((1^{st} (2^{nd} (x)) Hom (A) 1^{st} (y)) \times (2^{nd} (2^{nd} (x)) Hom (C) 2^{nd} (y))) \to 1^{st} (g) \in (1^{st} (2^{nd} (x)) Hom (A) 1^{st} (y))$
77	75 76	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 1^{st} (g) \in (1^{st} (2^{nd} (x)) Hom (A) 1^{st} (y))$
78	10 12 14 28 48 49 54 58 61 72 77	comfeqval	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f) = 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (B) 1^{st} (y)) 1^{st} (f)$
79	3	ad4antr	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
80	4	ad4antr	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
81		xp2nd	$⊢ 1^{st} (x) \in ({Base}_{A} \times {Base}_{C}) \to 2^{nd} (1^{st} (x)) \in {Base}_{C}$
82	52 81	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 2^{nd} (1^{st} (x)) \in {Base}_{C}$
83		xp2nd	$⊢ 2^{nd} (x) \in ({Base}_{A} \times {Base}_{C}) \to 2^{nd} (2^{nd} (x)) \in {Base}_{C}$
84	56 83	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 2^{nd} (2^{nd} (x)) \in {Base}_{C}$
85		xp2nd	$⊢ y \in ({Base}_{A} \times {Base}_{C}) \to 2^{nd} (y) \in {Base}_{C}$
86	59 85	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 2^{nd} (y) \in {Base}_{C}$
87		xp2nd	$⊢ f \in ((1^{st} (1^{st} (x)) Hom (A) 1^{st} (2^{nd} (x))) \times (2^{nd} (1^{st} (x)) Hom (C) 2^{nd} (2^{nd} (x)))) \to 2^{nd} (f) \in (2^{nd} (1^{st} (x)) Hom (C) 2^{nd} (2^{nd} (x)))$
88	70 87	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 2^{nd} (f) \in (2^{nd} (1^{st} (x)) Hom (C) 2^{nd} (2^{nd} (x)))$
89		xp2nd	$⊢ g \in ((1^{st} (2^{nd} (x)) Hom (A) 1^{st} (y)) \times (2^{nd} (2^{nd} (x)) Hom (C) 2^{nd} (y))) \to 2^{nd} (g) \in (2^{nd} (2^{nd} (x)) Hom (C) 2^{nd} (y))$
90	75 89	syl	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 2^{nd} (g) \in (2^{nd} (2^{nd} (x)) Hom (C) 2^{nd} (y))$
91	11 13 15 29 79 80 82 84 86 88 90	comfeqval	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f) = 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (D) 2^{nd} (y)) 2^{nd} (f)$
92	78 91	opeq12d	$⊢ ((((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y)) \land f \in Hom (A \times_{c} C) (x)) \to ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f)⟩ = ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (B) 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)⟩$
93	92	3impa	$⊢ (((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \land g \in (2^{nd} (x) Hom (A \times_{c} C) y) \land f \in Hom (A \times_{c} C) (x)) \to ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f)⟩ = ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (B) 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)⟩$
94	93	mpoeq3dva	$⊢ ((φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C}))) \land y \in ({Base}_{A} \times {Base}_{C})) \to (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f)⟩) = (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (B) 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)⟩)$
95	94	3impa	$⊢ (φ \land x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})) \land y \in ({Base}_{A} \times {Base}_{C})) \to (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f)⟩) = (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (B) 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)⟩)$
96	95	mpoeq3dva	$⊢ φ \to (x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})), y \in ({Base}_{A} \times {Base}_{C}) ⟼ (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f)⟩)) = (x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})), y \in ({Base}_{A} \times {Base}_{C}) ⟼ (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (B) 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)⟩))$
97	23 24 25 26 27 28 29 6 8 32 47 96	xpcval	$⊢ φ \to B \times_{c} D = \{⟨{Base}_{ndx}, {Base}_{A} \times {Base}_{C}⟩, ⟨Hom (ndx), Hom (A \times_{c} C)⟩, ⟨comp (ndx), (x \in (({Base}_{A} \times {Base}_{C}) \times ({Base}_{A} \times {Base}_{C})), y \in ({Base}_{A} \times {Base}_{C}) ⟼ (g \in (2^{nd} (x) Hom (A \times_{c} C) y), f \in Hom (A \times_{c} C) (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (A) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (C) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\}$
98	22 97	eqtr4d	$⊢ φ \to A \times_{c} C = B \times_{c} D$

Metamath Proof Explorer

Theorem xpcpropd

Proof