iscatd

Description: Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	iscatd.b	$⊢ φ \to B = {Base}_{C}$
	iscatd.h	$⊢ φ \to H = Hom (C)$
	iscatd.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
	iscatd.c	$⊢ φ \to C \in V$
	iscatd.1	$⊢ (φ \land x \in B) \to \underset{˙}{1} \in (x H x)$
	iscatd.2	$⊢ (φ \land (x \in B \land y \in B \land f \in (y H x))) \to \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f$
	iscatd.3	$⊢ (φ \land (x \in B \land y \in B \land f \in (x H y))) \to f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f$
	iscatd.4	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land (f \in (x H y) \land g \in (y H z))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
	iscatd.5	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B)) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)$
Assertion	iscatd	$⊢ φ \to C \in Cat$

Proof

Step	Hyp	Ref	Expression
1		iscatd.b	$⊢ φ \to B = {Base}_{C}$
2		iscatd.h	$⊢ φ \to H = Hom (C)$
3		iscatd.o	$⊢ φ \to \underset{˙}{\cdot} = comp (C)$
4		iscatd.c	$⊢ φ \to C \in V$
5		iscatd.1	$⊢ (φ \land x \in B) \to \underset{˙}{1} \in (x H x)$
6		iscatd.2	$⊢ (φ \land (x \in B \land y \in B \land f \in (y H x))) \to \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f$
7		iscatd.3	$⊢ (φ \land (x \in B \land y \in B \land f \in (x H y))) \to f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f$
8		iscatd.4	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land (f \in (x H y) \land g \in (y H z))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
9		iscatd.5	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B)) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)$
10	6	3exp2	$⊢ φ \to (x \in B \to (y \in B \to (f \in (y H x) \to \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f)))$
11	10	imp31	$⊢ ((φ \land x \in B) \land y \in B) \to (f \in (y H x) \to \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f)$
12	11	ralrimiv	$⊢ ((φ \land x \in B) \land y \in B) \to \forall f \in (y H x) \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f$
13	7	3exp2	$⊢ φ \to (x \in B \to (y \in B \to (f \in (x H y) \to f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f)))$
14	13	imp31	$⊢ ((φ \land x \in B) \land y \in B) \to (f \in (x H y) \to f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f)$
15	14	ralrimiv	$⊢ ((φ \land x \in B) \land y \in B) \to \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f$
16	12 15	jca	$⊢ ((φ \land x \in B) \land y \in B) \to (\forall f \in (y H x) \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f)$
17	16	ralrimiva	$⊢ (φ \land x \in B) \to \forall y \in B (\forall f \in (y H x) \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f)$
18		oveq1	$⊢ g = \underset{˙}{1} \to g (⟨y, x⟩ \underset{˙}{\cdot} x) f = \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f$
19	18	eqeq1d	$⊢ g = \underset{˙}{1} \to (g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \leftrightarrow \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f)$
20	19	ralbidv	$⊢ g = \underset{˙}{1} \to (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \leftrightarrow \forall f \in (y H x) \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f)$
21		oveq2	$⊢ g = \underset{˙}{1} \to f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1}$
22	21	eqeq1d	$⊢ g = \underset{˙}{1} \to (f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f)$
23	22	ralbidv	$⊢ g = \underset{˙}{1} \to (\forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f)$
24	20 23	anbi12d	$⊢ g = \underset{˙}{1} \to ((\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \leftrightarrow (\forall f \in (y H x) \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f))$
25	24	ralbidv	$⊢ g = \underset{˙}{1} \to (\forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \leftrightarrow \forall y \in B (\forall f \in (y H x) \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f))$
26	25	rspcev	$⊢ (\underset{˙}{1} \in (x H x) \land \forall y \in B (\forall f \in (y H x) \underset{˙}{1} (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) \underset{˙}{1} = f)) \to \exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f)$
27	5 17 26	syl2anc	$⊢ (φ \land x \in B) \to \exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f)$
28	8	3expia	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to ((f \in (x H y) \land g \in (y H z)) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z))$
29	28	3exp2	$⊢ φ \to (x \in B \to (y \in B \to (z \in B \to ((f \in (x H y) \land g \in (y H z)) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)))))$
30	29	imp43	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to ((f \in (x H y) \land g \in (y H z)) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z))$
31	9	3expa	$⊢ ((φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B))) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)$
32	31	3exp2	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B))) \to (f \in (x H y) \to (g \in (y H z) \to (k \in (z H w) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))))$
33	32	imp32	$⊢ ((φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B))) \land (f \in (x H y) \land g \in (y H z))) \to (k \in (z H w) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))$
34	33	ralrimiv	$⊢ ((φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B))) \land (f \in (x H y) \land g \in (y H z))) \to \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)$
35	34	ex	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in B \land w \in B))) \to ((f \in (x H y) \land g \in (y H z)) \to \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))$
36	35	expr	$⊢ (φ \land (x \in B \land y \in B)) \to ((z \in B \land w \in B) \to ((f \in (x H y) \land g \in (y H z)) \to \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)))$
37	36	expd	$⊢ (φ \land (x \in B \land y \in B)) \to (z \in B \to (w \in B \to ((f \in (x H y) \land g \in (y H z)) \to \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))))$
38	37	expr	$⊢ (φ \land x \in B) \to (y \in B \to (z \in B \to (w \in B \to ((f \in (x H y) \land g \in (y H z)) \to \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)))))$
39	38	imp42	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land w \in B) \to ((f \in (x H y) \land g \in (y H z)) \to \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))$
40	39	ralrimdva	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to ((f \in (x H y) \land g \in (y H z)) \to \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))$
41	30 40	jcad	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to ((f \in (x H y) \land g \in (y H z)) \to (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)))$
42	41	ralrimivv	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))$
43	42	ralrimivva	$⊢ (φ \land x \in B) \to \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))$
44	27 43	jca	$⊢ (φ \land x \in B) \to (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)))$
45	44	ralrimiva	$⊢ φ \to \forall x \in B (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)))$
46	2	oveqd	$⊢ φ \to x H x = x Hom (C) x$
47	2	oveqd	$⊢ φ \to y H x = y Hom (C) x$
48	3	oveqd	$⊢ φ \to ⟨y, x⟩ \underset{˙}{\cdot} x = ⟨y, x⟩ comp (C) x$
49	48	oveqd	$⊢ φ \to g (⟨y, x⟩ \underset{˙}{\cdot} x) f = g (⟨y, x⟩ comp (C) x) f$
50	49	eqeq1d	$⊢ φ \to (g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \leftrightarrow g (⟨y, x⟩ comp (C) x) f = f)$
51	47 50	raleqbidv	$⊢ φ \to (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \leftrightarrow \forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f)$
52	2	oveqd	$⊢ φ \to x H y = x Hom (C) y$
53	3	oveqd	$⊢ φ \to ⟨x, x⟩ \underset{˙}{\cdot} y = ⟨x, x⟩ comp (C) y$
54	53	oveqd	$⊢ φ \to f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f (⟨x, x⟩ comp (C) y) g$
55	54	eqeq1d	$⊢ φ \to (f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow f (⟨x, x⟩ comp (C) y) g = f)$
56	52 55	raleqbidv	$⊢ φ \to (\forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f \leftrightarrow \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)$
57	51 56	anbi12d	$⊢ φ \to ((\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \leftrightarrow (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f))$
58	1 57	raleqbidv	$⊢ φ \to (\forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \leftrightarrow \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f))$
59	46 58	rexeqbidv	$⊢ φ \to (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \leftrightarrow \exists g \in (x Hom (C) x) \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f))$
60	2	oveqd	$⊢ φ \to y H z = y Hom (C) z$
61	3	oveqd	$⊢ φ \to ⟨x, y⟩ \underset{˙}{\cdot} z = ⟨x, y⟩ comp (C) z$
62	61	oveqd	$⊢ φ \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g (⟨x, y⟩ comp (C) z) f$
63	2	oveqd	$⊢ φ \to x H z = x Hom (C) z$
64	62 63	eleq12d	$⊢ φ \to (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \leftrightarrow g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z))$
65	2	oveqd	$⊢ φ \to z H w = z Hom (C) w$
66	3	oveqd	$⊢ φ \to ⟨x, y⟩ \underset{˙}{\cdot} w = ⟨x, y⟩ comp (C) w$
67	3	oveqd	$⊢ φ \to ⟨y, z⟩ \underset{˙}{\cdot} w = ⟨y, z⟩ comp (C) w$
68	67	oveqd	$⊢ φ \to k (⟨y, z⟩ \underset{˙}{\cdot} w) g = k (⟨y, z⟩ comp (C) w) g$
69		eqidd	$⊢ φ \to f = f$
70	66 68 69	oveq123d	$⊢ φ \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f$
71	3	oveqd	$⊢ φ \to ⟨x, z⟩ \underset{˙}{\cdot} w = ⟨x, z⟩ comp (C) w$
72		eqidd	$⊢ φ \to k = k$
73	71 72 62	oveq123d	$⊢ φ \to k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f)$
74	70 73	eqeq12d	$⊢ φ \to ((k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) \leftrightarrow (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f))$
75	65 74	raleqbidv	$⊢ φ \to (\forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) \leftrightarrow \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f))$
76	1 75	raleqbidv	$⊢ φ \to (\forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) \leftrightarrow \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f))$
77	64 76	anbi12d	$⊢ φ \to ((g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \leftrightarrow (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f)))$
78	60 77	raleqbidv	$⊢ φ \to (\forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \leftrightarrow \forall g \in (y Hom (C) z) (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f)))$
79	52 78	raleqbidv	$⊢ φ \to (\forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \leftrightarrow \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f)))$
80	1 79	raleqbidv	$⊢ φ \to (\forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \leftrightarrow \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f)))$
81	1 80	raleqbidv	$⊢ φ \to (\forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \leftrightarrow \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f)))$
82	59 81	anbi12d	$⊢ φ \to ((\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))) \leftrightarrow (\exists g \in (x Hom (C) x) \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f))))$
83	1 82	raleqbidv	$⊢ φ \to (\forall x \in B (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))) \leftrightarrow \forall x \in {Base}_{C} (\exists g \in (x Hom (C) x) \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f))))$
84	45 83	mpbid	$⊢ φ \to \forall x \in {Base}_{C} (\exists g \in (x Hom (C) x) \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f)))$
85		eqid	$⊢ {Base}_{C} = {Base}_{C}$
86		eqid	$⊢ Hom (C) = Hom (C)$
87		eqid	$⊢ comp (C) = comp (C)$
88	85 86 87	iscat	$⊢ C \in V \to (C \in Cat \leftrightarrow \forall x \in {Base}_{C} (\exists g \in (x Hom (C) x) \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f))))$
89	4 88	syl	$⊢ φ \to (C \in Cat \leftrightarrow \forall x \in {Base}_{C} (\exists g \in (x Hom (C) x) \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z) \land \forall w \in {Base}_{C} \forall k \in (z Hom (C) w) (k (⟨y, z⟩ comp (C) w) g) (⟨x, y⟩ comp (C) w) f = k (⟨x, z⟩ comp (C) w) (g (⟨x, y⟩ comp (C) z) f))))$
90	84 89	mpbird	$⊢ φ \to C \in Cat$

Metamath Proof Explorer

Theorem iscatd

Proof