Theorem ismona 10737

Description: Monomorphisms of a category.

Hypotheses

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

Assertion

Ref	Expression
ismona	|- (T e. Cat -> (Monic` T) = {f | (f e. M /\ A.g e. M A.h e. M (((D` g) = (D` h) /\ (C` g) = (D` f) /\ (C` h) = (D` f)) -> ((fRg) = (fRh) -> g = h)))})

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

Proof of Theorem ismona

Step	Hyp	Ref	Expression
1		fveq2 3724	. . . . . . 7 |- (x = T -> (dom` x) = (dom` T))
2	1	dmeqd 3313	. . . . . 6 |- (x = T -> dom (dom` x) = dom (dom` T))
3		ismona.1	. . . . . 6 |- M = dom (dom` T)
4	2, 3	syl6eqr 1525	. . . . 5 |- (x = T -> dom (dom` x) = M)
5	4	eleq2d 1541	. . . 4 |- (x = T -> (f e. dom (dom` x) <-> f e. M))
6	4	raleq1d 1789	. . . . . 6 |- (x = T -> (A.h e. dom (dom` x)((((dom` x)` g) = ((dom` x)` h) /\ ((cod` x)` g) = ((dom` x)` f) /\ ((cod` x)` h) = ((dom` x)` f)) -> ((f(o` x)g) = (f(o` x)h) -> g = h)) <-> A.h e. M ((((dom` x)` g) = ((dom` x)` h) /\ ((cod` x)` g) = ((dom` x)` f) /\ ((cod` x)` h) = ((dom` x)` f)) -> ((f(o` x)g) = (f(o` x)h) -> g = h))))
7	6	ralbidv 1663	. . . . 5 |- (x = T -> (A.g e. dom (dom` x)A.h e. dom (dom` x)((((dom` x)` g) = ((dom` x)` h) /\ ((cod` x)` g) = ((dom` x)` f) /\ ((cod` x)` h) = ((dom` x)` f)) -> ((f(o` x)g) = (f(o` x)h) -> g = h)) <-> A.g e. dom (dom` x)A.h e. M ((((dom` x)` g) = ((dom` x)` h) /\ ((cod` x)` g) = ((dom` x)` f) /\ ((cod` x)` h) = ((dom` x)` f)) -> ((f(o` x)g) = (f(o` x)h) -> g = h))))
8	4	raleq1d 1789	. . . . 5 |- (x = T -> (A.g e. dom (dom` x)A.h e. M ((((dom` x)` g) = ((dom` x)` h) /\ ((cod` x)` g) = ((dom` x)` f) /\ ((cod` x)` h) = ((dom` x)` f)) -> ((f(o` x)g) = (f(o` x)h) -> g = h)) <-> A.g e. M A.h e. M ((((dom` x)` g) = ((dom` x)` h) /\ ((cod` x)` g) = ((dom` x)` f) /\ ((cod` x)` h) = ((dom` x)` f)) -> ((f(o` x)g) = (f(o` x)h) -> g = h))))
9	1	fveq1d 3726	. . . . . . . . . 10 |- (x = T -> ((dom` x)` g) = ((dom` T)` g))
10		ismona.2	. . . . . . . . . . . 12 |- D = (dom` T)
11	10	eqcomi 1479	. . . . . . . . . . 11 |- (dom` T) = D
12	11	fveq1i 3725	. . . . . . . . . 10 |- ((dom` T)` g) = (D` g)
13	9, 12	syl6eq 1523	. . . . . . . . 9 |- (x = T -> ((dom` x)` g) = (D` g))
14	1	fveq1d 3726	. . . . . . . . . 10 |- (x = T -> ((dom` x)` h) = ((dom` T)` h))
15	11	fveq1i 3725	. . . . . . . . . 10 |- ((dom` T)` h) = (D` h)
16	14, 15	syl6eq 1523	. . . . . . . . 9 |- (x = T -> ((dom` x)` h) = (D` h))
17	13, 16	eqeq12d 1489	. . . . . . . 8 |- (x = T -> (((dom` x)` g) = ((dom` x)` h) <-> (D` g) = (D` h)))
18		fveq2 3724	. . . . . . . . . . 11 |- (x = T -> (cod` x) = (cod` T))
19	18	fveq1d 3726	. . . . . . . . . 10 |- (x = T -> ((cod` x)` g) = ((cod` T)` g))
20		ismona.3	. . . . . . . . . . . 12 |- C = (cod` T)
21	20	eqcomi 1479	. . . . . . . . . . 11 |- (cod` T) = C
22	21	fveq1i 3725	. . . . . . . . . 10 |- ((cod` T)` g) = (C` g)
23	19, 22	syl6eq 1523	. . . . . . . . 9 |- (x = T -> ((cod` x)` g) = (C` g))
24	1	fveq1d 3726	. . . . . . . . . 10 |- (x = T -> ((dom` x)` f) = ((dom` T)` f))
25	11	fveq1i 3725	. . . . . . . . . 10 |- ((dom` T)` f) = (D` f)
26	24, 25	syl6eq 1523	. . . . . . . . 9 |- (x = T -> ((dom` x)` f) = (D` f))
27	23, 26	eqeq12d 1489	. . . . . . . 8 |- (x = T -> (((cod` x)` g) = ((dom` x)` f) <-> (C` g) = (D` f)))
28	18	fveq1d 3726	. . . . . . . . . 10 |- (x = T -> ((cod` x)` h) = ((cod` T)` h))
29	21	fveq1i 3725	. . . . . . . . . 10 |- ((cod` T)` h) = (C` h)
30	28, 29	syl6eq 1523	. . . . . . . . 9 |- (x = T -> ((cod` x)` h) = (C` h))
31	30, 26	eqeq12d 1489	. . . . . . . 8 |- (x = T -> (((cod` x)` h) = ((dom` x)` f) <-> (C` h) = (D` f)))
32	17, 27, 31	3anbi123d 893	. . . . . . 7 |- (x = T -> ((((dom` x)` g) = ((dom` x)` h) /\ ((cod` x)` g) = ((dom` x)` f) /\ ((cod` x)` h) = ((dom` x)` f)) <-> ((D` g) = (D` h) /\ (C` g) = (D` f) /\ (C` h) = (D` f))))
33		fveq2 3724	. . . . . . . . . . 11 |- (x = T -> (o` x) = (o` T))
34	33	opreqd 3977	. . . . . . . . . 10 |- (x = T -> (f(o` x)g) = (f(o` T)g))
35	33	opreqd 3977	. . . . . . . . . 10 |- (x = T -> (f(o` x)h) = (f(o` T)h))
36	34, 35	eqeq12d 1489	. . . . . . . . 9 |- (x = T -> ((f(o` x)g) = (f(o` x)h) <-> (f(o` T)g) = (f(o` T)h)))
37		ismona.4	. . . . . . . . . . 11 |- R = (o` T)
38		opreq 3967	. . . . . . . . . . . 12 |- ((o` T) = R -> (f(o` T)g) = (fRg))
39	38	eqcoms 1478	. . . . . . . . . . 11 |- (R = (o` T) -> (f(o` T)g) = (fRg))
40	37, 39	ax-mp 7	. . . . . . . . . 10 |- (f(o` T)g) = (fRg)
41		opreq 3967	. . . . . . . . . . . 12 |- ((o` T) = R -> (f(o` T)h) = (fRh))
42	41	eqcoms 1478	. . . . . . . . . . 11 |- (R = (o` T) -> (f(o` T)h) = (fRh))
43	37, 42	ax-mp 7	. . . . . . . . . 10 |- (f(o` T)h) = (fRh)
44	40, 43	eqeq12i 1488	. . . . . . . . 9 |- ((f(o` T)g) = (f(o` T)h) <-> (fRg) = (fRh))
45	36, 44	syl6bb 536	. . . . . . . 8 |- (x = T -> ((f(o` x)g) = (f(o` x)h) <-> (fRg) = (fRh)))
46	45	imbi1d 613	. . . . . . 7 |- (x = T -> (((f(o` x)g) = (f(o` x)h) -> g = h) <-> ((fRg) = (fRh) -> g = h)))
47	32, 46	imbi12d 626	. . . . . 6 |- (x = T -> (((((dom` x)` g) = ((dom` x)` h) /\ ((cod` x)` g) = ((dom` x)` f) /\ ((cod` x)` h) = ((dom` x)` f)) -> ((f(o` x)g) = (f(o` x)h) -> g = h)) <-> (((D` g) = (D` h) /\ (C` g) = (D` f) /\ (C` h) = (D` f)) -> ((fRg) = (fRh) -> g = h))))
48	47	2ralbidv 1680	. . . . 5 |- (x = T -> (A.g e. M A.h e. M ((((dom` x)` g) = ((dom` x)` h) /\ ((cod` x)` g) = ((dom` x)` f) /\ ((cod` x)` h) = ((dom` x)` f)) -> ((f(o` x)g) = (f(o` x)h) -> g = h)) <-> A.g e. M A.h e. M (((D` g) = (D` h) /\ (C` g) = (D` f) /\ (C` h) = (D` f)) -> ((fRg) = (fRh) -> g = h))))
49	7, 8, 48	3bitrd 544	. . . 4 |- (x = T -> (A.g e. dom (dom` x)A.h e. dom (dom` x)((((dom` x)` g) = ((dom` x)` h)