Theorem ismonc 10620

Description: The predicate "is a monomorphism" when F belongs to a homset .

Hypotheses

Ref	Expression
ismonc.1	|- O = dom (id` T)
ismonc.2	|- H = (hom` T)
ismonc.3	|- R = (o` T)

Assertion

Ref	Expression
ismonc	|- ((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) -> (F e. (Monic` T) <-> A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h)))

Distinct variable groups:   B,a,g,h   C,a,g,h   F,a,g,h   H,a,g,h   O,a,g,h   R,a   T,a,g,h

Proof of Theorem ismonc

Step	Hyp	Ref	Expression
1		eqid 1473	. . . 4 |- dom (dom` T) = dom (dom` T)
2		eqid 1473	. . . 4 |- (dom` T) = (dom` T)
3		eqid 1473	. . . 4 |- (cod` T) = (cod` T)
4		ismonc.3	. . . 4 |- R = (o` T)
5	1, 2, 3, 4	ismonb 10616	. . 3 |- ((T e. Cat /\ F e. (H` <.B, C>.)) -> (F e. (Monic` T) <-> (F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))))
6	5	3adant2 797	. 2 |- ((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) -> (F e. (Monic` T) <-> (F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))))
7		ax-17 969	. . . . . . . . . . 11 |- (((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ a e. O) -> A.g((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ a e. O))
8		ax-17 969	. . . . . . . . . . . 12 |- (F e. dom (dom` T) -> A.g F e. dom (dom` T))
9		hbra1 1684	. . . . . . . . . . . 12 |- (A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)) -> A.gA.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))
10	8, 9	hban 1007	. . . . . . . . . . 11 |- ((F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h))) -> A.g(F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h))))
11	7, 10	hban 1007	. . . . . . . . . 10 |- ((((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ a e. O) /\ (F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))) -> A.g(((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ a e. O) /\ (F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))))
12		ax-17 969	. . . . . . . . . . . 12 |- (((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ a e. O) -> A.h((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ a e. O))
13		ax-17 969	. . . . . . . . . . . . 13 |- (F e. dom (dom` T) -> A.h F e. dom (dom` T))
14		ax-17 969	. . . . . . . . . . . . . 14 |- (g e. dom (dom` T) -> A.h g e. dom (dom` T))
15		hbra1 1684	. . . . . . . . . . . . . 14 |- (A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)) -> A.hA.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))
16	14, 15	hbral 1683	. . . . . . . . . . . . 13 |- (A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)) -> A.hA.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))
17	13, 16	hban 1007	. . . . . . . . . . . 12 |- ((F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h))) -> A.h(F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h))))
18	12, 17	hban 1007	. . . . . . . . . . 11 |- ((((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ a e. O) /\ (F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))) -> A.h(((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ a e. O) /\ (F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))