xpccatid

Description: The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpccat.t	$⊢ T = C \times_{c} D$
	xpccat.c	$⊢ φ \to C \in Cat$
	xpccat.d	$⊢ φ \to D \in Cat$
	xpccat.x	$⊢ X = {Base}_{C}$
	xpccat.y	$⊢ Y = {Base}_{D}$
	xpccat.i	$⊢ I = Id (C)$
	xpccat.j	$⊢ J = Id (D)$
Assertion	xpccatid	$⊢ φ \to (T \in Cat \land Id (T) = (x \in X, y \in Y ⟼ ⟨I (x), J (y)⟩))$

Proof

Step	Hyp	Ref	Expression
1		xpccat.t	$⊢ T = C \times_{c} D$
2		xpccat.c	$⊢ φ \to C \in Cat$
3		xpccat.d	$⊢ φ \to D \in Cat$
4		xpccat.x	$⊢ X = {Base}_{C}$
5		xpccat.y	$⊢ Y = {Base}_{D}$
6		xpccat.i	$⊢ I = Id (C)$
7		xpccat.j	$⊢ J = Id (D)$
8	1 4 5	xpcbas	$⊢ X \times Y = {Base}_{T}$
9	8	a1i	$⊢ φ \to X \times Y = {Base}_{T}$
10		eqidd	$⊢ φ \to Hom (T) = Hom (T)$
11		eqidd	$⊢ φ \to comp (T) = comp (T)$
12	1	ovexi	$⊢ T \in V$
13	12	a1i	$⊢ φ \to T \in V$
14		biid	$⊢ ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v))) \leftrightarrow ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))$
15		eqid	$⊢ Hom (C) = Hom (C)$
16	2	adantr	$⊢ (φ \land t \in (X \times Y)) \to C \in Cat$
17		xp1st	$⊢ t \in (X \times Y) \to 1^{st} (t) \in X$
18	17	adantl	$⊢ (φ \land t \in (X \times Y)) \to 1^{st} (t) \in X$
19	4 15 6 16 18	catidcl	$⊢ (φ \land t \in (X \times Y)) \to I (1^{st} (t)) \in (1^{st} (t) Hom (C) 1^{st} (t))$
20		eqid	$⊢ Hom (D) = Hom (D)$
21	3	adantr	$⊢ (φ \land t \in (X \times Y)) \to D \in Cat$
22		xp2nd	$⊢ t \in (X \times Y) \to 2^{nd} (t) \in Y$
23	22	adantl	$⊢ (φ \land t \in (X \times Y)) \to 2^{nd} (t) \in Y$
24	5 20 7 21 23	catidcl	$⊢ (φ \land t \in (X \times Y)) \to J (2^{nd} (t)) \in (2^{nd} (t) Hom (D) 2^{nd} (t))$
25	19 24	opelxpd	$⊢ (φ \land t \in (X \times Y)) \to ⟨I (1^{st} (t)), J (2^{nd} (t))⟩ \in ((1^{st} (t) Hom (C) 1^{st} (t)) \times (2^{nd} (t) Hom (D) 2^{nd} (t)))$
26		eqid	$⊢ Hom (T) = Hom (T)$
27		simpr	$⊢ (φ \land t \in (X \times Y)) \to t \in (X \times Y)$
28	1 8 15 20 26 27 27	xpchom	$⊢ (φ \land t \in (X \times Y)) \to t Hom (T) t = (1^{st} (t) Hom (C) 1^{st} (t)) \times (2^{nd} (t) Hom (D) 2^{nd} (t))$
29	25 28	eleqtrrd	$⊢ (φ \land t \in (X \times Y)) \to ⟨I (1^{st} (t)), J (2^{nd} (t))⟩ \in (t Hom (T) t)$
30		fvex	$⊢ I (1^{st} (t)) \in V$
31		fvex	$⊢ J (2^{nd} (t)) \in V$
32	30 31	op1st	$⊢ 1^{st} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) = I (1^{st} (t))$
33	32	oveq1i	$⊢ 1^{st} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (t)) 1^{st} (f) = I (1^{st} (t)) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (t)) 1^{st} (f)$
34	2	adantr	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to C \in Cat$
35		simpr1l	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to s \in (X \times Y)$
36		xp1st	$⊢ s \in (X \times Y) \to 1^{st} (s) \in X$
37	35 36	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (s) \in X$
38		eqid	$⊢ comp (C) = comp (C)$
39		simpr1r	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to t \in (X \times Y)$
40	39 17	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (t) \in X$
41		simpr31	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to f \in (s Hom (T) t)$
42	1 8 15 20 26 35 39	xpchom	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to s Hom (T) t = (1^{st} (s) Hom (C) 1^{st} (t)) \times (2^{nd} (s) Hom (D) 2^{nd} (t))$
43	41 42	eleqtrd	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to f \in ((1^{st} (s) Hom (C) 1^{st} (t)) \times (2^{nd} (s) Hom (D) 2^{nd} (t)))$
44		xp1st	$⊢ f \in ((1^{st} (s) Hom (C) 1^{st} (t)) \times (2^{nd} (s) Hom (D) 2^{nd} (t))) \to 1^{st} (f) \in (1^{st} (s) Hom (C) 1^{st} (t))$
45	43 44	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (f) \in (1^{st} (s) Hom (C) 1^{st} (t))$
46	4 15 6 34 37 38 40 45	catlid	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to I (1^{st} (t)) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (t)) 1^{st} (f) = 1^{st} (f)$
47	33 46	syl5eq	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (t)) 1^{st} (f) = 1^{st} (f)$
48	30 31	op2nd	$⊢ 2^{nd} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) = J (2^{nd} (t))$
49	48	oveq1i	$⊢ 2^{nd} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (t)) 2^{nd} (f) = J (2^{nd} (t)) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (t)) 2^{nd} (f)$
50	3	adantr	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to D \in Cat$
51		xp2nd	$⊢ s \in (X \times Y) \to 2^{nd} (s) \in Y$
52	35 51	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (s) \in Y$
53		eqid	$⊢ comp (D) = comp (D)$
54	39 22	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (t) \in Y$
55		xp2nd	$⊢ f \in ((1^{st} (s) Hom (C) 1^{st} (t)) \times (2^{nd} (s) Hom (D) 2^{nd} (t))) \to 2^{nd} (f) \in (2^{nd} (s) Hom (D) 2^{nd} (t))$
56	43 55	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (f) \in (2^{nd} (s) Hom (D) 2^{nd} (t))$
57	5 20 7 50 52 53 54 56	catlid	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to J (2^{nd} (t)) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (t)) 2^{nd} (f) = 2^{nd} (f)$
58	49 57	syl5eq	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (t)) 2^{nd} (f) = 2^{nd} (f)$
59	47 58	opeq12d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to ⟨1^{st} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (t)) 1^{st} (f), 2^{nd} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (t)) 2^{nd} (f)⟩ = ⟨1^{st} (f), 2^{nd} (f)⟩$
60		eqid	$⊢ comp (T) = comp (T)$
61	39 29	syldan	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to ⟨I (1^{st} (t)), J (2^{nd} (t))⟩ \in (t Hom (T) t)$
62	1 8 26 38 53 60 35 39 39 41 61	xpcco	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to ⟨I (1^{st} (t)), J (2^{nd} (t))⟩ (⟨s, t⟩ comp (T) t) f = ⟨1^{st} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (t)) 1^{st} (f), 2^{nd} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (t)) 2^{nd} (f)⟩$
63		1st2nd2	$⊢ f \in ((1^{st} (s) Hom (C) 1^{st} (t)) \times (2^{nd} (s) Hom (D) 2^{nd} (t))) \to f = ⟨1^{st} (f), 2^{nd} (f)⟩$
64	43 63	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to f = ⟨1^{st} (f), 2^{nd} (f)⟩$
65	59 62 64	3eqtr4d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to ⟨I (1^{st} (t)), J (2^{nd} (t))⟩ (⟨s, t⟩ comp (T) t) f = f$
66	32	oveq2i	$⊢ 1^{st} (g) (⟨1^{st} (t), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) = 1^{st} (g) (⟨1^{st} (t), 1^{st} (t)⟩ comp (C) 1^{st} (u)) I (1^{st} (t))$
67		simpr2l	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to u \in (X \times Y)$
68		xp1st	$⊢ u \in (X \times Y) \to 1^{st} (u) \in X$
69	67 68	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (u) \in X$
70		simpr32	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to g \in (t Hom (T) u)$
71	1 8 15 20 26 39 67	xpchom	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to t Hom (T) u = (1^{st} (t) Hom (C) 1^{st} (u)) \times (2^{nd} (t) Hom (D) 2^{nd} (u))$
72	70 71	eleqtrd	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to g \in ((1^{st} (t) Hom (C) 1^{st} (u)) \times (2^{nd} (t) Hom (D) 2^{nd} (u)))$
73		xp1st	$⊢ g \in ((1^{st} (t) Hom (C) 1^{st} (u)) \times (2^{nd} (t) Hom (D) 2^{nd} (u))) \to 1^{st} (g) \in (1^{st} (t) Hom (C) 1^{st} (u))$
74	72 73	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (g) \in (1^{st} (t) Hom (C) 1^{st} (u))$
75	4 15 6 34 40 38 69 74	catrid	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (g) (⟨1^{st} (t), 1^{st} (t)⟩ comp (C) 1^{st} (u)) I (1^{st} (t)) = 1^{st} (g)$
76	66 75	syl5eq	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (g) (⟨1^{st} (t), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) = 1^{st} (g)$
77	48	oveq2i	$⊢ 2^{nd} (g) (⟨2^{nd} (t), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) = 2^{nd} (g) (⟨2^{nd} (t), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) J (2^{nd} (t))$
78		xp2nd	$⊢ u \in (X \times Y) \to 2^{nd} (u) \in Y$
79	67 78	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (u) \in Y$
80		xp2nd	$⊢ g \in ((1^{st} (t) Hom (C) 1^{st} (u)) \times (2^{nd} (t) Hom (D) 2^{nd} (u))) \to 2^{nd} (g) \in (2^{nd} (t) Hom (D) 2^{nd} (u))$
81	72 80	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (g) \in (2^{nd} (t) Hom (D) 2^{nd} (u))$
82	5 20 7 50 54 53 79 81	catrid	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (g) (⟨2^{nd} (t), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) J (2^{nd} (t)) = 2^{nd} (g)$
83	77 82	syl5eq	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (g) (⟨2^{nd} (t), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩) = 2^{nd} (g)$
84	76 83	opeq12d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to ⟨1^{st} (g) (⟨1^{st} (t), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩), 2^{nd} (g) (⟨2^{nd} (t), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩)⟩ = ⟨1^{st} (g), 2^{nd} (g)⟩$
85	1 8 26 38 53 60 39 39 67 61 70	xpcco	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to g (⟨t, t⟩ comp (T) u) ⟨I (1^{st} (t)), J (2^{nd} (t))⟩ = ⟨1^{st} (g) (⟨1^{st} (t), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩), 2^{nd} (g) (⟨2^{nd} (t), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (⟨I (1^{st} (t)), J (2^{nd} (t))⟩)⟩$
86		1st2nd2	$⊢ g \in ((1^{st} (t) Hom (C) 1^{st} (u)) \times (2^{nd} (t) Hom (D) 2^{nd} (u))) \to g = ⟨1^{st} (g), 2^{nd} (g)⟩$
87	72 86	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to g = ⟨1^{st} (g), 2^{nd} (g)⟩$
88	84 85 87	3eqtr4d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to g (⟨t, t⟩ comp (T) u) ⟨I (1^{st} (t)), J (2^{nd} (t))⟩ = g$
89	4 15 38 34 37 40 69 45 74	catcocl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f) \in (1^{st} (s) Hom (C) 1^{st} (u))$
90	5 20 53 50 52 54 79 56 81	catcocl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f) \in (2^{nd} (s) Hom (D) 2^{nd} (u))$
91	89 90	opelxpd	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to ⟨1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f)⟩ \in ((1^{st} (s) Hom (C) 1^{st} (u)) \times (2^{nd} (s) Hom (D) 2^{nd} (u)))$
92	1 8 26 38 53 60 35 39 67 41 70	xpcco	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to g (⟨s, t⟩ comp (T) u) f = ⟨1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f)⟩$
93	1 8 15 20 26 35 67	xpchom	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to s Hom (T) u = (1^{st} (s) Hom (C) 1^{st} (u)) \times (2^{nd} (s) Hom (D) 2^{nd} (u))$
94	91 92 93	3eltr4d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to g (⟨s, t⟩ comp (T) u) f \in (s Hom (T) u)$
95		simpr2r	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to v \in (X \times Y)$
96		xp1st	$⊢ v \in (X \times Y) \to 1^{st} (v) \in X$
97	95 96	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (v) \in X$
98		simpr33	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to h \in (u Hom (T) v)$
99	1 8 15 20 26 67 95	xpchom	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to u Hom (T) v = (1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v))$
100	98 99	eleqtrd	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to h \in ((1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v)))$
101		xp1st	$⊢ h \in ((1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v))) \to 1^{st} (h) \in (1^{st} (u) Hom (C) 1^{st} (v))$
102	100 101	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (h) \in (1^{st} (u) Hom (C) 1^{st} (v))$
103	4 15 38 34 37 40 69 45 74 97 102	catass	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to (1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g)) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (v)) 1^{st} (f) = 1^{st} (h) (⟨1^{st} (s), 1^{st} (u)⟩ comp (C) 1^{st} (v)) (1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f))$
104	1 8 26 38 53 60 39 67 95 70 98	xpcco	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to h (⟨t, u⟩ comp (T) v) g = ⟨1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g), 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)⟩$
105	104	fveq2d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (h (⟨t, u⟩ comp (T) v) g) = 1^{st} (⟨1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g), 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)⟩)$
106		ovex	$⊢ 1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g) \in V$
107		ovex	$⊢ 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g) \in V$
108	106 107	op1st	$⊢ 1^{st} (⟨1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g), 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)⟩) = 1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g)$
109	105 108	eqtrdi	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (h (⟨t, u⟩ comp (T) v) g) = 1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g)$
110	109	oveq1d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (h (⟨t, u⟩ comp (T) v) g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (v)) 1^{st} (f) = (1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g)) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (v)) 1^{st} (f)$
111	92	fveq2d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (g (⟨s, t⟩ comp (T) u) f) = 1^{st} (⟨1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f)⟩)$
112		ovex	$⊢ 1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f) \in V$
113		ovex	$⊢ 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f) \in V$
114	112 113	op1st	$⊢ 1^{st} (⟨1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f)⟩) = 1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f)$
115	111 114	eqtrdi	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (g (⟨s, t⟩ comp (T) u) f) = 1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f)$
116	115	oveq2d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (h) (⟨1^{st} (s), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g (⟨s, t⟩ comp (T) u) f) = 1^{st} (h) (⟨1^{st} (s), 1^{st} (u)⟩ comp (C) 1^{st} (v)) (1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f))$
117	103 110 116	3eqtr4d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (h (⟨t, u⟩ comp (T) v) g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (v)) 1^{st} (f) = 1^{st} (h) (⟨1^{st} (s), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g (⟨s, t⟩ comp (T) u) f)$
118		xp2nd	$⊢ v \in (X \times Y) \to 2^{nd} (v) \in Y$
119	95 118	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (v) \in Y$
120		xp2nd	$⊢ h \in ((1^{st} (u) Hom (C) 1^{st} (v)) \times (2^{nd} (u) Hom (D) 2^{nd} (v))) \to 2^{nd} (h) \in (2^{nd} (u) Hom (D) 2^{nd} (v))$
121	100 120	syl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (h) \in (2^{nd} (u) Hom (D) 2^{nd} (v))$
122	5 20 53 50 52 54 79 56 81 119 121	catass	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to (2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (v)) 2^{nd} (f) = 2^{nd} (h) (⟨2^{nd} (s), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) (2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f))$
123	104	fveq2d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (h (⟨t, u⟩ comp (T) v) g) = 2^{nd} (⟨1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g), 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)⟩)$
124	106 107	op2nd	$⊢ 2^{nd} (⟨1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g), 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)⟩) = 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)$
125	123 124	eqtrdi	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (h (⟨t, u⟩ comp (T) v) g) = 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)$
126	125	oveq1d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (h (⟨t, u⟩ comp (T) v) g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (v)) 2^{nd} (f) = (2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (v)) 2^{nd} (f)$
127	92	fveq2d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (g (⟨s, t⟩ comp (T) u) f) = 2^{nd} (⟨1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f)⟩)$
128	112 113	op2nd	$⊢ 2^{nd} (⟨1^{st} (g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (u)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f)⟩) = 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f)$
129	127 128	eqtrdi	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (g (⟨s, t⟩ comp (T) u) f) = 2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f)$
130	129	oveq2d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (h) (⟨2^{nd} (s), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g (⟨s, t⟩ comp (T) u) f) = 2^{nd} (h) (⟨2^{nd} (s), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) (2^{nd} (g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (u)) 2^{nd} (f))$
131	122 126 130	3eqtr4d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (h (⟨t, u⟩ comp (T) v) g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (v)) 2^{nd} (f) = 2^{nd} (h) (⟨2^{nd} (s), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g (⟨s, t⟩ comp (T) u) f)$
132	117 131	opeq12d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to ⟨1^{st} (h (⟨t, u⟩ comp (T) v) g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (v)) 1^{st} (f), 2^{nd} (h (⟨t, u⟩ comp (T) v) g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (v)) 2^{nd} (f)⟩ = ⟨1^{st} (h) (⟨1^{st} (s), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g (⟨s, t⟩ comp (T) u) f), 2^{nd} (h) (⟨2^{nd} (s), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g (⟨s, t⟩ comp (T) u) f)⟩$
133	4 15 38 34 40 69 97 74 102	catcocl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g) \in (1^{st} (t) Hom (C) 1^{st} (v))$
134	5 20 53 50 54 79 119 81 121	catcocl	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g) \in (2^{nd} (t) Hom (D) 2^{nd} (v))$
135	133 134	opelxpd	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to ⟨1^{st} (h) (⟨1^{st} (t), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g), 2^{nd} (h) (⟨2^{nd} (t), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g)⟩ \in ((1^{st} (t) Hom (C) 1^{st} (v)) \times (2^{nd} (t) Hom (D) 2^{nd} (v)))$
136	1 8 15 20 26 39 95	xpchom	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to t Hom (T) v = (1^{st} (t) Hom (C) 1^{st} (v)) \times (2^{nd} (t) Hom (D) 2^{nd} (v))$
137	135 104 136	3eltr4d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to h (⟨t, u⟩ comp (T) v) g \in (t Hom (T) v)$
138	1 8 26 38 53 60 35 39 95 41 137	xpcco	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to (h (⟨t, u⟩ comp (T) v) g) (⟨s, t⟩ comp (T) v) f = ⟨1^{st} (h (⟨t, u⟩ comp (T) v) g) (⟨1^{st} (s), 1^{st} (t)⟩ comp (C) 1^{st} (v)) 1^{st} (f), 2^{nd} (h (⟨t, u⟩ comp (T) v) g) (⟨2^{nd} (s), 2^{nd} (t)⟩ comp (D) 2^{nd} (v)) 2^{nd} (f)⟩$
139	1 8 26 38 53 60 35 67 95 94 98	xpcco	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to h (⟨s, u⟩ comp (T) v) (g (⟨s, t⟩ comp (T) u) f) = ⟨1^{st} (h) (⟨1^{st} (s), 1^{st} (u)⟩ comp (C) 1^{st} (v)) 1^{st} (g (⟨s, t⟩ comp (T) u) f), 2^{nd} (h) (⟨2^{nd} (s), 2^{nd} (u)⟩ comp (D) 2^{nd} (v)) 2^{nd} (g (⟨s, t⟩ comp (T) u) f)⟩$
140	132 138 139	3eqtr4d	$⊢ (φ \land ((s \in (X \times Y) \land t \in (X \times Y)) \land (u \in (X \times Y) \land v \in (X \times Y)) \land (f \in (s Hom (T) t) \land g \in (t Hom (T) u) \land h \in (u Hom (T) v)))) \to (h (⟨t, u⟩ comp (T) v) g) (⟨s, t⟩ comp (T) v) f = h (⟨s, u⟩ comp (T) v) (g (⟨s, t⟩ comp (T) u) f)$
141	9 10 11 13 14 29 65 88 94 140	iscatd2	$⊢ φ \to (T \in Cat \land Id (T) = (t \in (X \times Y) ⟼ ⟨I (1^{st} (t)), J (2^{nd} (t))⟩))$
142		vex	$⊢ x \in V$
143		vex	$⊢ y \in V$
144	142 143	op1std	$⊢ t = ⟨x, y⟩ \to 1^{st} (t) = x$
145	144	fveq2d	$⊢ t = ⟨x, y⟩ \to I (1^{st} (t)) = I (x)$
146	142 143	op2ndd	$⊢ t = ⟨x, y⟩ \to 2^{nd} (t) = y$
147	146	fveq2d	$⊢ t = ⟨x, y⟩ \to J (2^{nd} (t)) = J (y)$
148	145 147	opeq12d	$⊢ t = ⟨x, y⟩ \to ⟨I (1^{st} (t)), J (2^{nd} (t))⟩ = ⟨I (x), J (y)⟩$
149	148	mpompt	$⊢ (t \in (X \times Y) ⟼ ⟨I (1^{st} (t)), J (2^{nd} (t))⟩) = (x \in X, y \in Y ⟼ ⟨I (x), J (y)⟩)$
150	149	eqeq2i	$⊢ Id (T) = (t \in (X \times Y) ⟼ ⟨I (1^{st} (t)), J (2^{nd} (t))⟩) \leftrightarrow Id (T) = (x \in X, y \in Y ⟼ ⟨I (x), J (y)⟩)$
151	150	anbi2i	$⊢ (T \in Cat \land Id (T) = (t \in (X \times Y) ⟼ ⟨I (1^{st} (t)), J (2^{nd} (t))⟩)) \leftrightarrow (T \in Cat \land Id (T) = (x \in X, y \in Y ⟼ ⟨I (x), J (y)⟩))$
152	141 151	sylib	$⊢ φ \to (T \in Cat \land Id (T) = (x \in X, y \in Y ⟼ ⟨I (x), J (y)⟩))$

Metamath Proof Explorer

Theorem xpccatid

Proof