Theorem cati 10659

Description: Properties of a category.

Hypotheses

Ref	Expression
cati.1	|- D = (dom` T)
cati.2	|- C = (cod` T)
cati.3	|- J = (id` T)
cati.4	|- R = (o` T)
cati.5	|- M = dom D
cati.6	|- O = dom J

Assertion

Ref	Expression
cati	|- (T 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 cati

Step	Hyp	Ref	Expression
1		df-cat 10657	. . 3 |- Cat = {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ ((<.<.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))) /\ (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))))}
2	1	eleq2i 1541	. 2 |- (T e. Cat <-> T e. {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ ((<.<.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))) /\ (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))))})
3		cati.1	. . . . . . 7 |- D = (dom` T)
4	3	domval 10626	. . . . . 6 |- D = (1st` (1st` T))
5	4	eqcomi 1482	. . . . 5 |- (1st` (1st` T)) = D
6	5	eqeq2i 1488	. . . 4 |- (d = (1st` (1st` T)) <-> d = D)
7		opeq1 2491	. . . . . . . 8 |- (d = D -> <.d, c>. = <.D, c>.)
8	7	opeq1d 2497	. . . . . . 7 |- (d = D -> <.<.d, c>., <.j, r>.>. = <.<.D, c>., <.j, r>.>.)
9	8	eleq1d 1543	. . . . . 6 |- (d = D -> (<.<.d, c>., <.j, r>.>. e. Ded <-> <.<.D, c>., <.j, r>.>. e. Ded))
10		dmeq 3317	. . . . . . . . . 10 |- (d = D -> dom d = dom D)
11		cati.5	. . . . . . . . . 10 |- M = dom D
12	10, 11	syl6eqr 1528	. . . . . . . . 9 |- (d = D -> dom d = M)
13	12	eleq2d 1544	. . . . . . . 8 |- (d = D -> (f e. dom d <-> f e. M))
14	12	eleq2d 1544	. . . . . . . . . 10 |- (d = D -> (g e. dom d <-> g e. M))
15	12	eleq2d 1544	. . . . . . . . . . . 12 |- (d = D -> (h e. dom d <-> h e. M))
16		fveq1 3729	. . . . . . . . . . . . . . 15 |- (d = D -> (d` h) = (D` h))
17	16	eqeq1d 1486	. . . . . . . . . . . . . 14 |- (d = D -> ((d` h) = (c` g) <-> (D` h) = (c` g)))
18		fveq1 3729	. . . . . . . . . . . . . . 15 |- (d = D -> (d` g) = (D` g))
19	18	eqeq1d 1486	. . . . . . . . . . . . . 14 |- (d = D -> ((d` g) = (c` f) <-> (D` g) = (c` f)))
20	17, 19	anbi12d 630	. . . . . . . . . . . . 13 |- (d = D -> (((d` h) = (c` g) /\ (d` g) = (c` f)) <-> ((D` h) = (c` g) /\ (D` g) = (c` f))))
21	20	imbi1d 615	. . . . . . . . . . . 12 |- (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))))
22	15, 21	imbi12d 628	. . . . . . . . . . 11 |- (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)))))
23	22	ralbidv2 1668	. . . . . . . . . 10 |- (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))))
24	14, 23	imbi12d 628	. . . . . . . . 9 |- (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)))))
25	24	ralbidv2 1668	. . . . . . . 8 |- (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))))
26	13, 25	imbi12d 628	. . . . . . 7 |- (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)))))
27	26	ralbidv2 1668	. . . . . 6 |- (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))))
28	9, 27	anbi12d 630	. . . . 5 |- (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)))))
29	12	raleq1d 1792	. . . . . . 7 |- (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)))
30	29	ralbidv 1666	. . . . . 6 |- (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)))
31		fveq1 3729	. . . . . . . . . . 11 |- (d = D -> (d` f) = (D` f))
32	31	eqeq1d 1486	. . . . . . . . . 10 |- (d = D -> ((d` f) = a <-> (D` f) = a))
33	32	imbi1d 615	. . . . . . . . 9 |-