Theorem cmpmon 10692

Description: The composite of two monomorphisms is a monomorphism. JFM CAT₁ th. 61

Hypotheses

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

Assertion

Ref	Expression
cmpmon	|- ((T e. Cat /\ ((A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) /\ (F e. (Monic` T) /\ G e. (Monic` T)))) -> (GRF) e. (Monic` T))

Proof of Theorem cmpmon

Step	Hyp	Ref	Expression
1		ax-17 970	. . . . . . . 8 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> A.a(T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))))
2		hbra1 1686	. . . . . . . . 9 |- (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) -> A.aA.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h))
3		hbra1 1686	. . . . . . . . 9 |- (A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l) -> A.aA.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))
4	2, 3	hban 1008	. . . . . . . 8 |- ((A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)) -> A.a(A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))
5	1, 4	hban 1008	. . . . . . 7 |- (((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) /\ (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))) -> A.a((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) /\ (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))))
6		ax-17 970	. . . . . . . . . . 11 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> A.g(T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))))
7		ax-17 970	. . . . . . . . . . . . 13 |- (a e. O -> A.g a e. O)
8		hbra1 1686	. . . . . . . . . . . . 13 |- (A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) -> A.gA.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h))
9	7, 8	hbral 1685	. . . . . . . . . . . 12 |- (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) -> A.gA.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h))
10		ax-17 970	. . . . . . . . . . . 12 |- (A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l) -> A.gA.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))
11	9, 10	hban 1008	. . . . . . . . . . 11 |- ((A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)) -> A.g(A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))
12	6, 11	hban 1008	. . . . . . . . . 10 |- (((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) /\ (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))) -> A.g((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) /\ (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))))
13	12, 7	hban 1008	. . . . . . . . 9 |- ((((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) /\ (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))) /\ a e. O) -> A.g(((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) /\ (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) /\ A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))) /\ a e. O))
14		ax-17 970	. . . . . . . . . . . . . 14 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> A.h(T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))))
15		ax-17 970	. . . . . . . . . . . . . . . 16 |- (a e. O -> A.h a e. O)
16		ax-17 970	. . . . . . . . . . . . . . . . 17 |- (g e. (H` <.a, A>.) -> A.h g e. (H` <.a, A>.))
17		hbra1 1686	. . . . . . . . . . . . . . . . 17 |- (A.h e. (H` <.a, A>.)((FRg) = (FRh