iscat

Description: The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	iscat.b	$⊢ B = {Base}_{C}$
	iscat.h	$⊢ H = Hom (C)$
	iscat.o	$⊢ \underset{˙}{\cdot} = comp (C)$
Assertion	iscat	$⊢ C \in V \to (C \in Cat \leftrightarrow \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))))$

Proof

Step	Hyp	Ref	Expression
1		iscat.b	$⊢ B = {Base}_{C}$
2		iscat.h	$⊢ H = Hom (C)$
3		iscat.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		fvexd	$⊢ c = C \to {Base}_{c} \in V$
5		fveq2	$⊢ c = C \to {Base}_{c} = {Base}_{C}$
6	5 1	eqtr4di	$⊢ c = C \to {Base}_{c} = B$
7		fvexd	$⊢ (c = C \land b = B) \to Hom (c) \in V$
8		simpl	$⊢ (c = C \land b = B) \to c = C$
9	8	fveq2d	$⊢ (c = C \land b = B) \to Hom (c) = Hom (C)$
10	9 2	eqtr4di	$⊢ (c = C \land b = B) \to Hom (c) = H$
11		fvexd	$⊢ ((c = C \land b = B) \land h = H) \to comp (c) \in V$
12		simpll	$⊢ ((c = C \land b = B) \land h = H) \to c = C$
13	12	fveq2d	$⊢ ((c = C \land b = B) \land h = H) \to comp (c) = comp (C)$
14	13 3	eqtr4di	$⊢ ((c = C \land b = B) \land h = H) \to comp (c) = \underset{˙}{\cdot}$
15		simpllr	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to b = B$
16		simplr	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to h = H$
17	16	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to x h x = x H x$
18	16	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to y h x = y H x$
19		simpr	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to o = \underset{˙}{\cdot}$
20	19	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ⟨y, x⟩ o x = ⟨y, x⟩ \underset{˙}{\cdot} x$
21	20	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to g (⟨y, x⟩ o x) f = g (⟨y, x⟩ \underset{˙}{\cdot} x) f$
22	21	eqeq1d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (g (⟨y, x⟩ o x) f = f \leftrightarrow g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f)$
23	18 22	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \leftrightarrow \forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f)$
24	16	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to x h y = x H y$
25	19	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ⟨x, x⟩ o y = ⟨x, x⟩ \underset{˙}{\cdot} y$
26	25	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to f (⟨x, x⟩ o y) g = f (⟨x, x⟩ \underset{˙}{\cdot} y) g$
27	26	eqeq1d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (f (⟨x, x⟩ o y) g = f \leftrightarrow f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f)$
28	24 27	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall f \in (x h y) f (⟨x, x⟩ o y) g = f \leftrightarrow \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f)$
29	23 28	anbi12d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ((\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o y) g = f) \leftrightarrow (\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))$
30	15 29	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o y) g = f) \leftrightarrow \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))$
31	17 30	rexeqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\exists g \in (x h x) \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o y) g = f) \leftrightarrow \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))$
32	16	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to y h z = y H z$
33	19	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ⟨x, y⟩ o z = ⟨x, y⟩ \underset{˙}{\cdot} z$
34	33	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to g (⟨x, y⟩ o z) f = g (⟨x, y⟩ \underset{˙}{\cdot} z) f$
35	16	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to x h z = x H z$
36	34 35	eleq12d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (g (⟨x, y⟩ o z) f \in (x h z) \leftrightarrow g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z))$
37	16	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to z h w = z H w$
38	19	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ⟨x, y⟩ o w = ⟨x, y⟩ \underset{˙}{\cdot} w$
39	19	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ⟨y, z⟩ o w = ⟨y, z⟩ \underset{˙}{\cdot} w$
40	39	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to k (⟨y, z⟩ o w) g = k (⟨y, z⟩ \underset{˙}{\cdot} w) g$
41		eqidd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to f = f$
42	38 40 41	oveq123d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f$
43	19	oveqd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ⟨x, z⟩ o w = ⟨x, z⟩ \underset{˙}{\cdot} w$
44		eqidd	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to k = k$
45	43 44 34	oveq123d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f) = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)$
46	42 45	eqeq12d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ((k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f) \leftrightarrow (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))$
47	37 46	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f) \leftrightarrow \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))$
48	15 47	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f) \leftrightarrow \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))$
49	36 48	anbi12d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ((g (⟨x, y⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f)) \leftrightarrow (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)))$
50	32 49	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall g \in (y h z) (g (⟨x, y⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f)) \leftrightarrow \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)))$
51	24 50	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall f \in (x h y) \forall g \in (y h z) (g (⟨x, y⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f)) \leftrightarrow \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)))$
52	15 51	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall z \in b \forall f \in (x h y) \forall g \in (y h z) (g (⟨x, y⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f)) \leftrightarrow \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)))$
53	15 52	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall y \in b \forall z \in b \forall f \in (x h y) \forall g \in (y h z) (g (⟨x, y⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f)) \leftrightarrow \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)))$
54	31 53	anbi12d	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to ((\exists g \in (x h x) \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o 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⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f))) \leftrightarrow (\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))))$
55	15 54	raleqbidv	$⊢ (((c = C \land b = B) \land h = H) \land o = \underset{˙}{\cdot}) \to (\forall x \in b (\exists g \in (x h x) \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o 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⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f))) \leftrightarrow \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))))$
56	11 14 55	sbcied2	$⊢ ((c = C \land b = B) \land h = H) \to (\underset{˙}{[} comp (c) / o \underset{˙}{]} \forall x \in b (\exists g \in (x h x) \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o 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⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f))) \leftrightarrow \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))))$
57	7 10 56	sbcied2	$⊢ (c = C \land b = B) \to (\underset{˙}{[} Hom (c) / h \underset{˙}{]} \underset{˙}{[} comp (c) / o \underset{˙}{]} \forall x \in b (\exists g \in (x h x) \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o 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⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f))) \leftrightarrow \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))))$
58	4 6 57	sbcied2	$⊢ c = C \to (\underset{˙}{[} {Base}_{c} / b \underset{˙}{]} \underset{˙}{[} Hom (c) / h \underset{˙}{]} \underset{˙}{[} comp (c) / o \underset{˙}{]} \forall x \in b (\exists g \in (x h x) \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o 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⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f))) \leftrightarrow \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))))$
59		df-cat	$⊢ Cat = \{c \| \underset{˙}{[} {Base}_{c} / b \underset{˙}{]} \underset{˙}{[} Hom (c) / h \underset{˙}{]} \underset{˙}{[} comp (c) / o \underset{˙}{]} \forall x \in b (\exists g \in (x h x) \forall y \in b (\forall f \in (y h x) g (⟨y, x⟩ o x) f = f \land \forall f \in (x h y) f (⟨x, x⟩ o 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⟩ o z) f \in (x h z) \land \forall w \in b \forall k \in (z h w) (k (⟨y, z⟩ o w) g) (⟨x, y⟩ o w) f = k (⟨x, z⟩ o w) (g (⟨x, y⟩ o z) f)))\}$
60	58 59	elab2g	$⊢ C \in V \to (C \in Cat \leftrightarrow \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))))$

Metamath Proof Explorer

Theorem iscat

Proof