Theorem isepia 10718

Description: Epimorphisms of a category T.

Hypotheses

Ref	Expression
isepia.1	|- M = dom (dom` T)
isepia.2	|- D = (dom` T)
isepia.3	|- C = (cod` T)
isepia.4	|- R = (o` T)

Assertion

Ref	Expression
isepia	|- (T e. Cat -> (Epi` T) = {f | (f e. M /\ A.g e. M A.h e. M (((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h)))})

Distinct variable groups:   f,M,g,h   T,f,g,h

Proof of Theorem isepia

Step	Hyp	Ref	Expression
1		fveq2 3730	. . . . . . 7 |- (x = T -> (dom` x) = (dom` T))
2	1	dmeqd 3319	. . . . . 6 |- (x = T -> dom (dom` x) = dom (dom` T))
3		isepia.1	. . . . . 6 |- M = dom (dom` T)
4	2, 3	syl6eqr 1528	. . . . 5 |- (x = T -> dom (dom` x) = M)
5	4	eleq2d 1544	. . . 4 |- (x = T -> (f e. dom (dom` x) <-> f e. M))
6		fveq2 3730	. . . . . . . . . . 11 |- (x = T -> (cod` x) = (cod` T))
7	6	fveq1d 3732	. . . . . . . . . 10 |- (x = T -> ((cod` x)` g) = ((cod` T)` g))
8		isepia.3	. . . . . . . . . . . . 13 |- C = (cod` T)
9	8	eqcomi 1482	. . . . . . . . . . . 12 |- (cod` T) = C
10	9	a1i 8	. . . . . . . . . . 11 |- (x = T -> (cod` T) = C)
11	10	fveq1d 3732	. . . . . . . . . 10 |- (x = T -> ((cod` T)` g) = (C` g))
12	7, 11	eqtrd 1510	. . . . . . . . 9 |- (x = T -> ((cod` x)` g) = (C` g))
13	6, 8	syl6eqr 1528	. . . . . . . . . 10 |- (x = T -> (cod` x) = C)
14	13	fveq1d 3732	. . . . . . . . 9 |- (x = T -> ((cod` x)` h) = (C` h))
15	12, 14	eqeq12d 1492	. . . . . . . 8 |- (x = T -> (((cod` x)` g) = ((cod` x)` h) <-> (C` g) = (C` h)))
16		isepia.2	. . . . . . . . . . 11 |- D = (dom` T)
17	1, 16	syl6eqr 1528	. . . . . . . . . 10 |- (x = T -> (dom` x) = D)
18	17	fveq1d 3732	. . . . . . . . 9 |- (x = T -> ((dom` x)` g) = (D` g))
19	6	fveq1d 3732	. . . . . . . . . 10 |- (x = T -> ((cod` x)` f) = ((cod` T)` f))
20	10	fveq1d 3732	. . . . . . . . . 10 |- (x = T -> ((cod` T)` f) = (C` f))
21	19, 20	eqtrd 1510	. . . . . . . . 9 |- (x = T -> ((cod` x)` f) = (C` f))
22	18, 21	eqeq12d 1492	. . . . . . . 8 |- (x = T -> (((dom` x)` g) = ((cod` x)` f) <-> (D` g) = (C` f)))
23	17	fveq1d 3732	. . . . . . . . 9 |- (x = T -> ((dom` x)` h) = (D` h))
24	23, 21	eqeq12d 1492	. . . . . . . 8 |- (x = T -> (((dom` x)` h) = ((cod` x)` f) <-> (D` h) = (C` f)))
25	15, 22, 24	3anbi123d 895	. . . . . . 7 |- (x = T -> ((((cod` x)` g) = ((cod` x)` h) /\ ((dom` x)` g) = ((cod` x)` f) /\ ((dom` x)` h) = ((cod` x)` f)) <-> ((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f))))
26		fveq2 3730	. . . . . . . . . . 11 |- (x = T -> (o` x) = (o` T))
27	26	opreqd 3983	. . . . . . . . . 10 |- (x = T -> (g(o` x)f) = (g(o` T)f))
28		isepia.4	. . . . . . . . . . . . 13 |- R = (o` T)
29	28	eqcomi 1482	. . . . . . . . . . . 12 |- (o` T) = R
30	29	a1i 8	. . . . . . . . . . 11 |- (x = T -> (o` T) = R)
31	30	opreqd 3983	. . . . . . . . . 10 |- (x = T -> (g(o` T)f) = (gRf))
32	27, 31	eqtrd 1510	. . . . . . . . 9 |- (x = T -> (g(o` x)f) = (gRf))
33	26	opreqd 3983	. . . . . . . . . 10 |- (x = T -> (h(o` x)f) = (h(o` T)f))
34	30	opreqd 3983	. . . . . . . . . 10 |- (x = T -> (h(o` T)f) = (hRf))
35	33, 34	eqtrd 1510	. . . . . . . . 9 |- (x = T -> (h(o` x)f) = (hRf))
36	32, 35	eqeq12d 1492	. . . . . . . 8 |- (x = T -> ((g(o` x)f) = (h(o` x)f) <-> (gRf) = (hRf)))
37	36	imbi1d 615	. . . . . . 7 |- (x = T -> (((g(o` x)f) = (h(o` x)f) -> g = h) <-> ((gRf) = (hRf) -> g = h)))
38	25, 37	imbi12d 628	. . . . . 6 |- (x = T -> (((((cod` x)` g) = ((cod` x)` h) /\ ((dom` x)` g) = ((cod` x)` f) /\ ((dom` x)` h) = ((cod` x)` f)) -> ((g(o` x)f) = (h(o` x)f) -> g = h)) <-> (((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h))))
39	38	2ralbidv 1683	. . . . 5 |- (x = T -> (A.g e. dom (dom` x)A.h e. dom (dom` x)((((cod` x)` g) = ((cod` x)` h) /\ ((dom` x)` g) = ((cod` x)` f) /\ ((dom` x)` h) = ((cod` x)` f)) -> ((g(o` x)f) = (h(o` x)f) -> g = h)) <-> A.g e. dom (dom` x)A.h e. dom (dom` x)(((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h))))
40	4	raleq1d 1792	. . . . . 6 |- (x = T -> (A.h e. dom (dom` x)(((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h)) <-> A.h e. M (((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h))))
41	40	ralbidv 1666	. . . . 5 |- (x = T -> (A.g e. dom (dom` x)A.h e. dom (dom` x)(((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h)) <-> A.g e. dom (dom` x)A.h e. M (((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h))))
42	4	raleq1d 1792	. . . . 5 |- (x = T -> (A.g e. dom (dom` x)A.h e. M (((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h)) <-> A.g e. M A.h e. M (((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h))))
43	39, 41, 42	3bitrd 546	. . . 4 |- (x = T -> (A.g e. dom (dom` x)A.h e. dom (dom` x)((((cod` x)` g) = ((cod` x)` h) /\ ((dom` x)` g) = ((cod` x)` f) /\ ((dom` x)` h) = ((cod` x)` f)) -> ((g(o` x)f) = (h(o` x)f) -> g = h)) <-> A.g e. M A.h e. M (((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h))))
44	5, 43	anbi12d 630	. . 3 |- (x = T -> ((f e. dom (dom` x) /\ A.g e. dom (dom` x)A.h e. dom (dom` x)((((cod` x)` g) = ((cod` x)` h) /\ ((dom` x)` g) = ((cod` x)` f) /\ ((dom` x)` h) = ((cod` x)` f)) -> ((g(o` x)f) = (h(o` x)f) -> g = h))) <-> (f e. M /\ A.g e. M A.h e. M (((C` g) = (C` h) /\ (D` g) = (C` f) /\ (D` h) = (C` f)) -> ((gRf) = (hRf) -> g = h)))))
45	44	abbidv 1580	. 2 |- (x = T