setccatid

		Ref	Expression
	Hypothesis	setccat.c	$⊢ C = SetCat (U)$
	Assertion	setccatid	$⊢ U \in V \to (C \in Cat \land Id (C) = (x \in U ⟼ {I ↾}_{x}))$

Proof

Step	Hyp	Ref	Expression
1		setccat.c	$⊢ C = SetCat (U)$
2		id	$⊢ U \in V \to U \in V$
3	1 2	setcbas	$⊢ U \in V \to U = {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 U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \leftrightarrow ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))$
9		f1oi	$⊢ ({I ↾}_{x}) : x \underset{1-1 onto}{⟶} x$
10		f1of	$⊢ ({I ↾}_{x}) : x \underset{1-1 onto}{⟶} x \to ({I ↾}_{x}) : x ⟶ x$
11	9 10	mp1i	$⊢ (U \in V \land x \in U) \to ({I ↾}_{x}) : x ⟶ x$
12		simpl	$⊢ (U \in V \land x \in U) \to U \in V$
13		eqid	$⊢ Hom (C) = Hom (C)$
14		simpr	$⊢ (U \in V \land x \in U) \to x \in U$
15	1 12 13 14 14	elsetchom	$⊢ (U \in V \land x \in U) \to ({I ↾}_{x} \in (x Hom (C) x) \leftrightarrow ({I ↾}_{x}) : x ⟶ x)$
16	11 15	mpbird	$⊢ (U \in V \land x \in U) \to {I ↾}_{x} \in (x Hom (C) x)$
17		simpl	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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$
18		eqid	$⊢ comp (C) = comp (C)$
19		simpr1l	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to w \in U$
20		simpr1r	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to x \in U$
21		simpr31	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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)$
22	1 17 13 19 20	elsetchom	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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) \leftrightarrow f : w ⟶ x)$
23	21 22	mpbid	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to f : w ⟶ x$
24	9 10	mp1i	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to ({I ↾}_{x}) : x ⟶ x$
25	1 17 18 19 20 20 23 24	setcco	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to ({I ↾}_{x}) (⟨w, x⟩ comp (C) x) f = ({I ↾}_{x}) \circ f$
26		fcoi2	$⊢ f : w ⟶ x \to ({I ↾}_{x}) \circ f = f$
27	23 26	syl	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to ({I ↾}_{x}) \circ f = f$
28	25 27	eqtrd	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to ({I ↾}_{x}) (⟨w, x⟩ comp (C) x) f = f$
29		simpr2l	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to y \in U$
30		simpr32	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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)$
31	1 17 13 20 29	elsetchom	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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) \leftrightarrow g : x ⟶ y)$
32	30 31	mpbid	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g : x ⟶ y$
33	1 17 18 20 20 29 24 32	setcco	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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) ({I ↾}_{x}) = g \circ ({I ↾}_{x})$
34		fcoi1	$⊢ g : x ⟶ y \to g \circ ({I ↾}_{x}) = g$
35	32 34	syl	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g \circ ({I ↾}_{x}) = g$
36	33 35	eqtrd	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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) ({I ↾}_{x}) = g$
37	1 17 18 19 20 29 23 32	setcco	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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 f$
38		fco	$⊢ (g : x ⟶ y \land f : w ⟶ x) \to (g \circ f) : w ⟶ y$
39	32 23 38	syl2anc	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (g \circ f) : w ⟶ y$
40	1 17 13 19 29	elsetchom	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (g \circ f \in (w Hom (C) y) \leftrightarrow (g \circ f) : w ⟶ y)$
41	39 40	mpbird	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g \circ f \in (w Hom (C) y)$
42	37 41	eqeltrd	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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)$
43		coass	$⊢ (h \circ g) \circ f = h \circ (g \circ f)$
44		simpr2r	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to z \in U$
45		simpr33	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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)$
46	1 17 13 29 44	elsetchom	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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) \leftrightarrow h : y ⟶ z)$
47	45 46	mpbid	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h : y ⟶ z$
48		fco	$⊢ (h : y ⟶ z \land g : x ⟶ y) \to (h \circ g) : x ⟶ z$
49	47 32 48	syl2anc	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h \circ g) : x ⟶ z$
50	1 17 18 19 20 44 23 49	setcco	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h \circ g) (⟨w, x⟩ comp (C) z) f = (h \circ g) \circ f$
51	1 17 18 19 29 44 39 47	setcco	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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 f) = h \circ (g \circ f)$
52	43 50 51	3eqtr4a	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h \circ g) (⟨w, x⟩ comp (C) z) f = h (⟨w, y⟩ comp (C) z) (g \circ f)$
53	1 17 18 20 29 44 32 47	setcco	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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 g$
54	53	oveq1d	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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 g) (⟨w, x⟩ comp (C) z) f$
55	37	oveq2d	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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 f)$
56	52 54 55	3eqtr4d	$⊢ (U \in V \land ((w \in U \land x \in U) \land (y \in U \land z \in U) \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 16 28 36 42 56	iscatd2	$⊢ U \in V \to (C \in Cat \land Id (C) = (x \in U ⟼ {I ↾}_{x}))$

Metamath Proof Explorer

Theorem setccatid

Proof