Theorem iscat 10658

Description: The predicate "is a category".

Hypotheses

Ref	Expression
iscat.1	|- M = dom D
iscat.2	|- O = dom J

Assertion

Ref	Expression
iscat	|- (((D e. A /\ C e. B /\ J e. F) /\ R e. G) -> (<.<.D, C>., <.J, R>.>. e. Cat <-> ((<.<.D, C>., <.J, R>.>. e. Ded /\ A.f e. M A.g e. M A.h e. M (((D` h) = (C` g) /\ (D` g) = (C` f)) -> (hR(gRf)) = ((hRg)Rf))) /\ (A.a e. O A.f e. M ((C` f) = a -> ((J` a)Rf) = f) /\ A.a e. O A.f e. M ((D` f) = a -> (fR(J` a)) = f)))))

Distinct variable groups:   C,a,f,g,h   D,a,f,g,h   J,a,f   f,M   R,a,f,g,h

Proof of Theorem iscat

Step	Hyp	Ref	Expression
1		opeq1 2491	. . . . . . 7 |- (d = D -> <.d, c>. = <.D, c>.)
2	1	opeq1d 2497	. . . . . 6 |- (d = D -> <.<.d, c>., <.j, r>.>. = <.<.D, c>., <.j, r>.>.)
3	2	eleq1d 1543	. . . . 5 |- (d = D -> (<.<.d, c>., <.j, r>.>. e. Ded <-> <.<.D, c>., <.j, r>.>. e. Ded))
4		dmeq 3317	. . . . . . . . 9 |- (d = D -> dom d = dom D)
5		iscat.1	. . . . . . . . 9 |- M = dom D
6	4, 5	syl6eqr 1528	. . . . . . . 8 |- (d = D -> dom d = M)
7	6	eleq2d 1544	. . . . . . 7 |- (d = D -> (f e. dom d <-> f e. M))
8	6	eleq2d 1544	. . . . . . . . 9 |- (d = D -> (g e. dom d <-> g e. M))
9	6	eleq2d 1544	. . . . . . . . . . 11 |- (d = D -> (h e. dom d <-> h e. M))
10		fveq1 3729	. . . . . . . . . . . . . 14 |- (d = D -> (d` h) = (D` h))
11	10	eqeq1d 1486	. . . . . . . . . . . . 13 |- (d = D -> ((d` h) = (c` g) <-> (D` h) = (c` g)))
12		fveq1 3729	. . . . . . . . . . . . . 14 |- (d = D -> (d` g) = (D` g))
13	12	eqeq1d 1486	. . . . . . . . . . . . 13 |- (d = D -> ((d` g) = (c` f) <-> (D` g) = (c` f)))
14	11, 13	anbi12d 630	. . . . . . . . . . . 12 |- (d = D -> (((d` h) = (c` g) /\ (d` g) = (c` f)) <-> ((D` h) = (c` g) /\ (D` g) = (c` f))))
15	14	imbi1d 615	. . . . . . . . . . 11 |- (d = D -> ((((d` h) = (c` g) /\ (d` g) = (c` f)) -> (hr(grf)) = ((hrg)rf)) <-> (((D` h) = (c` g) /\ (D` g) = (c` f)) -> (hr(grf)) = ((hrg)rf))))
16	9, 15	imbi12d 628	. . . . . . . . . 10 |- (d = D -> ((h e. dom d -> (((d` h) = (c` g) /\ (d` g) = (c` f)) -> (hr(grf)) = ((hrg)rf))) <-> (h e. M -> (((D` h) = (c` g) /\ (D` g) = (c` f)) -> (hr(grf)) = ((hrg)rf)))))
17	16	ralbidv2 1668	. . . . . . . . 9 |- (d = D -> (A.h e. dom d(((d` h) = (c` g) /\ (d` g) = (c` f)) -> (hr(grf)) = ((hrg)rf)) <-> A.h e. M (((D` h) = (c` g) /\ (D` g) = (c` f)) -> (hr(grf)) = ((hrg)rf))))
18	8, 17	imbi12d 628	. . . . . . . 8 |- (d = D -> ((g e. dom d -> A.h e. dom d(((d` h) = (c` g) /\ (d` g) = (c` f)) -> (hr(grf)) = ((hrg)rf))) <-> (g e. M -> A.h e. M (((D` h) = (c` g) /\ (D` g) = (c` f)) -> (hr(grf)) = ((hrg)rf)))))
19	18	ralbidv2 1668	. . . . . . 7 |- (d = D -> (A.g e. dom dA.h e. dom d(((d` h) = (c` g) /\ (d` g) = (c` f)) -> (hr(grf)) = ((hrg)rf)) <-> A.g e. M A.h e. M (((D` h) = (c` g) /\ (D` g) = (c` f)) -> (hr(grf)) = ((hrg)rf))))
20	7, 19	imbi12d 628	. . . . . 6 |- (d = D -> ((f e. dom d -> A.g e. dom dA.h e. dom d(((d` h) = (c` g) /\ (d` g) = (c` f)) -> (hr(grf)) = ((hrg)rf))) <-> (f e. M -> A.g e. M A.h e. M (((D` h) = (c` g) /\ (D` g) = (c` f)) -> (hr(grf)) = ((hrg)rf)))))
21	20	ralbidv2 1668	. . . . 5 |- (d = D -> (A.f e. dom dA.g e. dom dA.h e. dom d(((d` h) = (c` g) /\ (d` g) = (c` f)) -> (hr(grf)) = ((hrg)rf)) <-> A.f e. M A.g e. M A.h e. M (((D` h) = (c` g) /\ (D` g) = (c` f)) -> (hr(grf)) = ((hrg)rf))))
22	3, 21	anbi12d 630	. . . 4 |- (d = D -> ((<.<.d, c>., <.j, r>.>. e. Ded /\ A.f e. dom dA.g e. dom dA.h e. dom d(((d` h) = (c` g) /\ (d` g) = (c` f)) -> (hr(grf)) = ((hrg)rf))) <-> (<.<.D, c>., <.j, r>.>. e. Ded /\ A.f e. M A.g e. M A.h e. M (((D` h) = (c` g) /\ (D` g) = (c` f)) -> (hr(grf)) = ((hrg)rf)))))
23	6	raleq1d 1792	. . . . . 6 |- (d = D -> (A.f e. dom d((c` f) = a -> ((j` a)rf) = f) <-> A.f e. M ((c` f) = a -> ((j` a)rf) = f)))
24	23	ralbidv 1666	. . . . 5 |- (d = D -> (A.a e. dom jA.f e. dom d((c` f) = a -> ((j` a)rf) = f) <-> A.a e. dom jA.f e. M ((c` f) = a -> ((j` a)rf) = f)))
25		fveq1 3729	. . . . . . . . . 10 |- (d = D -> (d` f) = (D` f))
26	25	eqeq1d 1486	. . . . . . . . 9 |- (d = D -> ((d` f) = a <-> (D` f) = a))
27	26	imbi1d 615	. . . . . . . 8 |- (d = D -> (((d` f) = a -> (fr(j` a)) = f) <-> ((D` f) = a -> (fr(j` a)) = f)))
28	7, 27	imbi12d 628	. . . . . . 7 |- (d = D -> ((f e. dom d -> ((d` f) = a -> (fr(j` a)) = f)) <-> (f e. M -> ((D` f) = a -> (fr(j` a)) = f))))
29	28	ralbidv2 1668	. . . . . 6 |- (d = D -> (A.f e. dom d((d` f) = a -> (fr(j` a)) = f) <-> A.f e. M ((D` f) = a -> (fr(j` a)) = f)))
30	29	ralbidv 1666	. . . . 5 |- (d = D -> (A.a e. dom jA.f e. dom d((d` f) = a -> (fr(j` a)) = f) <-> A.a e. dom jA.f e. M ((D` f) = a -> (fr(j` a)) = f)))
31	24, 30	anbi12d 630	. . . 4 |- (d = D -> ((A.a e. dom jA.f e. dom d((c` f) = a -> ((j` a)rf) = f) /\ A.a e. dom jA.f e. dom d((d` f) = a -> (fr(j` a)) = f)) <-> (A.a e. dom jA.f e. M ((c` f) = a -> ((j` a)rf) = f) /\ A.a e. dom jA.f e. M ((D` f) = a -> (fr(j` a)) = f))))
32	22, 31	anbi12d 630	. . 3 |- (d = D -> (((<.<.d, c>., <.j, r>.>. e. Ded /\ A.f e. dom