Theorem icmpmon 10587

Description: If (GRF) is monic then F is monic. JFM CAT₁ th. 62

Hypotheses

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

Assertion

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

Proof of Theorem icmpmon

Step	Hyp	Ref	Expression
1		icmpmon.1	. . . . . . 7 |- O = dom (id` T)
2		icmpmon.2	. . . . . . 7 |- H = (hom` T)
3		icmpmon.3	. . . . . . 7 |- R = (o` T)
4	1, 2, 3	ismonc 10584	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ C e. O) /\ (GRF) e. (H` <.A, C>.)) -> ((GRF) e. (Monic` T) <-> A.a e. O A.m e. (H` <.a, A>.)A.n e. (H` <.a, A>.)(((GRF)Rm) = ((GRF)Rn) -> m = n)))
5		3simp1 786	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> T e. Cat)
6		3simpb 784	. . . . . . 7 |- ((A e. O /\ B e. O /\ C e. O) -> (A e. O /\ C e. O))
7	6	3ad2ant2 799	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> (A e. O /\ C e. O))
8	1, 2, 3	homgrf 10574	. . . . . . 7 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O)) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GRF) e. (H` <.A, C>.)))
9	8	3impia 828	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> (GRF) e. (H` <.A, C>.))
10	4, 5, 7, 9	syl3anc 856	. . . . 5 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> ((GRF) e. (Monic` T) <-> A.a e. O A.m e. (H` <.a, A>.)A.n e. (H` <.a, A>.)(((GRF)Rm) = ((GRF)Rn) -> m = n)))
11		pm3.27 323	. . . . . . . . . . . . 13 |- (((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) /\ (GR(FRm)) = (GR(FRn))) -> (GR(FRm)) = (GR(FRn)))
12		simpll 412	. . . . . . . . . . . . 13 |- (((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) /\ (GR(FRm)) = (GR(FRn))) -> ((GRF)Rm) = (GR(FRm)))
13		simplr 413	. . . . . . . . . . . . 13 |- (((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) /\ (GR(FRm)) = (GR(FRn))) -> ((GRF)Rn) = (GR(FRn)))
14	11, 12, 13	3eqtr4d 1509	. . . . . . . . . . . 12 |- (((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) /\ (GR(FRm)) = (GR(FRn))) -> ((GRF)Rm) = ((GRF)Rn))
15	14	ex 373	. . . . . . . . . . 11 |- ((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) -> ((GR(FRm)) = (GR(FRn)) -> ((GRF)Rm) = ((GRF)Rn)))
16	15	imim1d 28	. . . . . . . . . 10 |- ((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) -> ((((GRF)Rm) = ((GRF)Rn) -> m = n) -> ((GR(FRm)) = (GR(FRn)) -> m = n)))
17		opreq2 3954	. . . . . . . . . 10 |- ((FRm) = (FRn) -> (GR(FRm)) = (GR(FRn)))
18	16, 17	syl7 23	. . . . . . . . 9 |- ((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) -> ((((GRF)Rm) = ((GRF)Rn) -> m = n) -> ((FRm) = (FRn) -> m = n)))
19	1, 2, 3	cmpassoh 10573	. . . . . . . . . . . . . . . . . . . . . 22 |- ((T e. Cat /\ (a e. O /\ A e. O) /\ (B e. O /\ C e. O)) -> ((m e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRm)) = ((GRF)Rm)))
20	19	3exp 830	. . . . . . . . . . . . . . . . . . . . 21 |- (T e. Cat -> ((a e. O /\ A e. O) -> ((B e. O /\ C e. O) -> ((m e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRm)) = ((GRF)Rm)))))
21	20	com3l 34	. . . . . . . . . . . . . . . . . . . 20 |- ((a e. O /\ A e. O) -> ((B e. O /\ C e. O) -> (T e. Cat -> ((m e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRm)) = ((GRF)Rm)))))
22	21	exp4b 379	. . . . . . . . . . . . . . . . . . 19 |- (a e. O -> (A e. O -> (B e. O -> (C e. O -> (T e. Cat -> ((m e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRm)) = ((GRF)Rm)))))))
23	22	3impd 845	. . . . . . . . . . . . . . . . . 18 |- (a e. O -> ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> ((m e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRm)) = ((GRF)Rm)))))
24	23	com13 33	. . . . . . . . . . . . . . . . 17 |- (T e. Cat -> ((A e. O /\ B e. O /\ C e. O) -> (a e. O -> ((m e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRm)) = ((GRF)Rm)))))
25	24	imp 350	. . . . . . . . . . . . . . . 16 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O)) -> (a e. O -> ((m e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRm)) = ((GRF)Rm))))
26	25	com13 33	. . . . . . . . . . . . . . 15 |- ((m e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (a e. O -> ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O)) -> (GR(FRm)) = ((GRF)Rm))))
27	26	3expib 834	. . . . . . . . . . . . . 14 |- (m e. (H` <.a, A>.) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (a e. O -> ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O)) -> (GR(FRm)) = ((GRF)Rm)))))
28	27	com14 38	. . . . . . . . . . . . 13 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O)) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (a e. O -> (m e. (H` <.a, A>.) -> (GR(FRm)) = ((GRF)Rm)))))
29	28	3impia 828	. . . . . . . . . . . 12 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.)