Metamath Proof Explorer


Theorem 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 · ˙ = comp C
Assertion iscat C V C Cat x B g x H x y B f y H x g y x · ˙ x f = f f x H y f x x · ˙ y g = f y B z B f x H y g y H z g x y · ˙ z f x H z w B k z H w k y z · ˙ w g x y · ˙ w f = k x z · ˙ w g x y · ˙ z f

Proof

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