estrccatid

		Ref	Expression
	Hypothesis	estrccat.c	$⊢ C = ExtStrCat (U)$
	Assertion	estrccatid	$⊢ U \in V \to (C \in Cat \land Id (C) = (x \in U ⟼ {I ↾}_{{Base}_{x}}))$

Proof

Step	Hyp	Ref	Expression
1		estrccat.c	$⊢ C = ExtStrCat (U)$
2		id	$⊢ U \in V \to U \in V$
3	1 2	estrcbas	$⊢ 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 ↾}_{{Base}_{x}}) : {Base}_{x} \underset{1-1 onto}{⟶} {Base}_{x}$
10		f1of	$⊢ ({I ↾}_{{Base}_{x}}) : {Base}_{x} \underset{1-1 onto}{⟶} {Base}_{x} \to ({I ↾}_{{Base}_{x}}) : {Base}_{x} ⟶ {Base}_{x}$
11	9 10	mp1i	$⊢ (U \in V \land x \in U) \to ({I ↾}_{{Base}_{x}}) : {Base}_{x} ⟶ {Base}_{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		eqid	$⊢ {Base}_{x} = {Base}_{x}$
16	1 12 13 14 14 15 15	elestrchom	$⊢ (U \in V \land x \in U) \to ({I ↾}_{{Base}_{x}} \in (x Hom (C) x) \leftrightarrow ({I ↾}_{{Base}_{x}}) : {Base}_{x} ⟶ {Base}_{x})$
17	11 16	mpbird	$⊢ (U \in V \land x \in U) \to {I ↾}_{{Base}_{x}} \in (x Hom (C) x)$
18		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$
19		eqid	$⊢ comp (C) = comp (C)$
20		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$
21		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$
22		eqid	$⊢ {Base}_{w} = {Base}_{w}$
23		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)$
24	1 18 13 20 21 22 15	elestrchom	$⊢ (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 : {Base}_{w} ⟶ {Base}_{x})$
25	23 24	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 : {Base}_{w} ⟶ {Base}_{x}$
26	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 ↾}_{{Base}_{x}}) : {Base}_{x} ⟶ {Base}_{x}$
27	1 18 19 20 21 21 22 15 15 25 26	estrcco	$⊢ (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 ↾}_{{Base}_{x}}) (⟨w, x⟩ comp (C) x) f = ({I ↾}_{{Base}_{x}}) \circ f$
28		fcoi2	$⊢ f : {Base}_{w} ⟶ {Base}_{x} \to ({I ↾}_{{Base}_{x}}) \circ f = f$
29	25 28	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 ↾}_{{Base}_{x}}) \circ f = f$
30	27 29	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 ↾}_{{Base}_{x}}) (⟨w, x⟩ comp (C) x) f = f$
31		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$
32		eqid	$⊢ {Base}_{y} = {Base}_{y}$
33		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)$
34	1 18 13 21 31 15 32	elestrchom	$⊢ (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 : {Base}_{x} ⟶ {Base}_{y})$
35	33 34	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 : {Base}_{x} ⟶ {Base}_{y}$
36	1 18 19 21 21 31 15 15 32 26 35	estrcco	$⊢ (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 ↾}_{{Base}_{x}}) = g \circ ({I ↾}_{{Base}_{x}})$
37		fcoi1	$⊢ g : {Base}_{x} ⟶ {Base}_{y} \to g \circ ({I ↾}_{{Base}_{x}}) = g$
38	35 37	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 ↾}_{{Base}_{x}}) = g$
39	36 38	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 ↾}_{{Base}_{x}}) = g$
40	1 18 19 20 21 31 22 15 32 25 35	estrcco	$⊢ (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$
41		fco	$⊢ (g : {Base}_{x} ⟶ {Base}_{y} \land f : {Base}_{w} ⟶ {Base}_{x}) \to (g \circ f) : {Base}_{w} ⟶ {Base}_{y}$
42	35 25 41	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) : {Base}_{w} ⟶ {Base}_{y}$
43	1 18 13 20 31 22 32	elestrchom	$⊢ (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) : {Base}_{w} ⟶ {Base}_{y})$
44	42 43	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)$
45	40 44	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)$
46		coass	$⊢ (h \circ g) \circ f = h \circ (g \circ f)$
47		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$
48		eqid	$⊢ {Base}_{z} = {Base}_{z}$
49		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)$
50	1 18 13 31 47 32 48	elestrchom	$⊢ (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 : {Base}_{y} ⟶ {Base}_{z})$
51	49 50	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 : {Base}_{y} ⟶ {Base}_{z}$
52		fco	$⊢ (h : {Base}_{y} ⟶ {Base}_{z} \land g : {Base}_{x} ⟶ {Base}_{y}) \to (h \circ g) : {Base}_{x} ⟶ {Base}_{z}$
53	51 35 52	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) : {Base}_{x} ⟶ {Base}_{z}$
54	1 18 19 20 21 47 22 15 48 25 53	estrcco	$⊢ (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$
55	1 18 19 20 31 47 22 32 48 42 51	estrcco	$⊢ (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)$
56	46 54 55	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)$
57	1 18 19 21 31 47 15 32 48 35 51	estrcco	$⊢ (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$
58	57	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$
59	40	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)$
60	56 58 59	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)$
61	3 4 5 7 8 17 30 39 45 60	iscatd2	$⊢ U \in V \to (C \in Cat \land Id (C) = (x \in U ⟼ {I ↾}_{{Base}_{x}}))$

Metamath Proof Explorer

Theorem estrccatid

Proof