catccatid

	Ref	Expression
Hypotheses	catccatid.c	$⊢ C = CatCat (U)$
	catccatid.b	$⊢ B = {Base}_{C}$
Assertion	catccatid	$⊢ U \in V \to (C \in Cat \land Id (C) = (x \in B ⟼ {id}_{func} (x)))$

Proof

Step	Hyp	Ref	Expression
1		catccatid.c	$⊢ C = CatCat (U)$
2		catccatid.b	$⊢ B = {Base}_{C}$
3	2	a1i	$⊢ U \in V \to B = {Base}_{C}$
4		eqidd	$⊢ U \in V \to Hom (C) = Hom (C)$
5		eqidd	$⊢ U \in V \to comp (C) = comp (C)$
6	1	fvexi	$⊢ C \in V$
7	6	a1i	$⊢ U \in V \to C \in V$
8		biid	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \leftrightarrow ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))$
9		id	$⊢ U \in V \to U \in V$
10	1 2 9	catcbas	$⊢ U \in V \to B = U \cap Cat$
11		inss2	$⊢ U \cap Cat \subseteq Cat$
12	10 11	eqsstrdi	$⊢ U \in V \to B \subseteq Cat$
13	12	sselda	$⊢ (U \in V \land x \in B) \to x \in Cat$
14		eqid	$⊢ {id}_{func} (x) = {id}_{func} (x)$
15	14	idfucl	$⊢ x \in Cat \to {id}_{func} (x) \in (x Func x)$
16	13 15	syl	$⊢ (U \in V \land x \in B) \to {id}_{func} (x) \in (x Func x)$
17		simpl	$⊢ (U \in V \land x \in B) \to U \in V$
18		eqid	$⊢ Hom (C) = Hom (C)$
19		simpr	$⊢ (U \in V \land x \in B) \to x \in B$
20	1 2 17 18 19 19	catchom	$⊢ (U \in V \land x \in B) \to x Hom (C) x = x Func x$
21	16 20	eleqtrrd	$⊢ (U \in V \land x \in B) \to {id}_{func} (x) \in (x Hom (C) x)$
22		simpl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to U \in V$
23		eqid	$⊢ comp (C) = comp (C)$
24		simpr1l	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to w \in B$
25		simpr1r	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to x \in B$
26		simpr31	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to f \in (w Hom (C) x)$
27	1 2 22 18 24 25	catchom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to w Hom (C) x = w Func x$
28	26 27	eleqtrd	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to f \in (w Func x)$
29	25 16	syldan	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to {id}_{func} (x) \in (x Func x)$
30	1 2 22 23 24 25 25 28 29	catcco	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to {id}_{func} (x) (⟨w, x⟩ comp (C) x) f = {id}_{func} (x) \circ_{func} f$
31	28 14	cofulid	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to {id}_{func} (x) \circ_{func} f = f$
32	30 31	eqtrd	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to {id}_{func} (x) (⟨w, x⟩ comp (C) x) f = f$
33		simpr2l	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to y \in B$
34		simpr32	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g \in (x Hom (C) y)$
35	1 2 22 18 25 33	catchom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to x Hom (C) y = x Func y$
36	34 35	eleqtrd	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g \in (x Func y)$
37	1 2 22 23 25 25 33 29 36	catcco	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g (⟨x, x⟩ comp (C) y) {id}_{func} (x) = g \circ_{func} {id}_{func} (x)$
38	36 14	cofurid	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g \circ_{func} {id}_{func} (x) = g$
39	37 38	eqtrd	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g (⟨x, x⟩ comp (C) y) {id}_{func} (x) = g$
40	28 36	cofucl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g \circ_{func} f \in (w Func y)$
41	1 2 22 23 24 25 33 28 36	catcco	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g (⟨w, x⟩ comp (C) y) f = g \circ_{func} f$
42	1 2 22 18 24 33	catchom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to w Hom (C) y = w Func y$
43	40 41 42	3eltr4d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g (⟨w, x⟩ comp (C) y) f \in (w Hom (C) y)$
44		simpr33	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h \in (y Hom (C) z)$
45		simpr2r	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to z \in B$
46	1 2 22 18 33 45	catchom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to y Hom (C) z = y Func z$
47	44 46	eleqtrd	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h \in (y Func z)$
48	28 36 47	cofuass	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h \circ_{func} g) \circ_{func} f = h \circ_{func} (g \circ_{func} f)$
49	36 47	cofucl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h \circ_{func} g \in (x Func z)$
50	1 2 22 23 24 25 45 28 49	catcco	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h \circ_{func} g) (⟨w, x⟩ comp (C) z) f = (h \circ_{func} g) \circ_{func} f$
51	1 2 22 23 24 33 45 40 47	catcco	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h (⟨w, y⟩ comp (C) z) (g \circ_{func} f) = h \circ_{func} (g \circ_{func} f)$
52	48 50 51	3eqtr4d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h \circ_{func} g) (⟨w, x⟩ comp (C) z) f = h (⟨w, y⟩ comp (C) z) (g \circ_{func} f)$
53	1 2 22 23 25 33 45 36 47	catcco	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h (⟨x, y⟩ comp (C) z) g = h \circ_{func} g$
54	53	oveq1d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h (⟨x, y⟩ comp (C) z) g) (⟨w, x⟩ comp (C) z) f = (h \circ_{func} g) (⟨w, x⟩ comp (C) z) f$
55	41	oveq2d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h (⟨w, y⟩ comp (C) z) (g (⟨w, x⟩ comp (C) y) f) = h (⟨w, y⟩ comp (C) z) (g \circ_{func} f)$
56	52 54 55	3eqtr4d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h (⟨x, y⟩ comp (C) z) g) (⟨w, x⟩ comp (C) z) f = h (⟨w, y⟩ comp (C) z) (g (⟨w, x⟩ comp (C) y) f)$
57	3 4 5 7 8 21 32 39 43 56	iscatd2	$⊢ U \in V \to (C \in Cat \land Id (C) = (x \in B ⟼ {id}_{func} (x)))$

Metamath Proof Explorer

Theorem catccatid

Proof