Theorem icmpmon 15165

Description: If (GRF) is a monomorphism then F is a monomorphism. 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		simp1 876	. . . . . 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 )
2		3simpb 873	. . . . . . 7 |- ((A e. O /\ B e. O /\ C e. O) -> (A e. O /\ C e. O))
3	2	3ad2ant2 898	. . . . . 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))
4		icmpmon.1	. . . . . . . 8 |- O = dom (id` T)
5		icmpmon.2	. . . . . . . 8 |- H = ( hom ` T)
6		icmpmon.3	. . . . . . . 8 |- R = (o` T)
7	4, 5, 6	homgrf 15151	. . . . . . 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>.)))
8	7	3impia 1064	. . . . . 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>.))
9	4, 5, 6	ismonc 15163	. . . . . 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)))
10	1, 3, 8, 9	syl111anc 1100	. . . . 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	4, 5, 6	cmpassoh 15150	. . . . . . . . . . . . . . . . . . . . . 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)))
12	11	3exp 1066	. . . . . . . . . . . . . . . . . . . . 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)))))
13	12	com3l 38	. . . . . . . . . . . . . . . . . . . 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)))))
14	13	exp4b 410	. . . . . . . . . . . . . . . . . . 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)))))))
15	14	3impd 1082	. . . . . . . . . . . . . . . . . 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)))))
16	15	com13 37	. . . . . . . . . . . . . . . . 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)))))
17	16	imp 377	. . . . . . . . . . . . . . . 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))))
18	17	com13 37	. . . . . . . . . . . . . . 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))))
19	18	3expib 1070	. . . . . . . . . . . . . 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)))))
20	19	com14 42	. . . . . . . . . . . . 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)))))
21	20	3impia 1064	. . . . . . . . . . . 12 |- ((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))))
22	21	imp31 389	. . . . . . . . . . 11 |- ((((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))
23	22	eqcomd 1889	. . . . . . . . . 10 |- ((((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>.)) -> ((GRF)Rm) = (GR(FRm)))
24	23	adantr 425	. . . . . . . . 9 |- (((((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>.)) /\ n e. (H` <.a, A>.)) -> ((GRF)Rm) = (GR(FRm)))
25	4, 5, 6	cmpassoh 15150	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((T e. Cat /\ (a e. O /\ A e. O) /\ (B e. O /\ C e. O)) -> ((n e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRn)) = ((GRF)Rn)))
26	25	imp 377	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((T e. Cat /\ (a e. O /\ A e. O) /\ (B e. O /\ C e. O)) /\ (n e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> (GR(FRn)) = ((GRF)Rn))
27	26	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . 22 |- (((T e. Cat /\ (a e. O /\ A e. O) /\ (B e. O /\ C e. O)) /\ (n e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> ((GRF)Rn) = (GR(FRn)))
28	27	3exp1 1084	. . . . . . . . . . . . . . . . . . . . 21 |- (T e. Cat -> ((a e. O /\ A e. O) -> ((B e. O /\ C e. O) -> ((n e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rn) = (GR(FRn))))))
29	28	com3l 38	. . . . . . . . . . . . . . . . . . . 20 |- ((a e. O /\ A e. O) -> ((B e. O /\ C e. O) -> (T e. Cat -> ((n e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rn) = (GR(FRn))))))
30	29	exp4b 410	. . . . . . . . . . . . . . . . . . 19 |- (a e. O -> (A e. O -> (B e. O -> (C e. O -> (T e. Cat -> ((n e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rn) = (GR(FRn))))))))
31	30	3impd 1082	. . . . . . . . . . . . . . . . . 18 |- (a e. O -> ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> ((n e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rn) = (GR(FRn))))))
32	31	com14 42	. . . . . . . . . . . . . . . . 17 |- ((n e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> (a e. O -> ((GRF)Rn) = (GR(FRn))))))
33	32	3expib 1070	. . . . . . . . . . . . . . . 16 |- (n e. (H` <.a, A>.) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> (a e. O -> ((GRF)Rn) = (GR(FRn)))))))
34	33	com23 36	. . . . . . . . . . . . . . 15 |- (n e. (H` <.a, A>.) -> ((A e. O /\ B e. O /\ C e. O) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (T e. Cat -> (a e. O -> ((GRF)Rn) = (GR(FRn)))))))
35	34	com14 42	. . . . . . . . . . . . . 14 |- (T e. Cat -> ((A e. O /\ B e. O /\ C e. O) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (n e. (H` <.a, A>.) -> (a e. O -> ((GRF)Rn) = (GR(FRn)))))))
36	35	3imp 1061	. . . . . . . . . . . . 13 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> (n e. (H` <.a, A>.) -> (a e. O -> ((GRF)Rn) = (GR(FRn)))))
37	36	com23 36	. . . . . . . . . . . 12 |- ((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 -> (n e. (H` <.a, A>.) -> ((GRF)Rn) = (GR(FRn)))))
38	37	imp 377	. . . . . . . . . . 11 |- (((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) -> (n e. (H` <.a, A>.) -> ((GRF)Rn) = (GR(FRn))))
39	38	adantr 425	. . . . . . . . . 10 |- ((((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>.)) -> (n e. (H` <.a, A>.) -> ((GRF)Rn) = (GR(FRn))))
40	39	imp 377	. . . . . . . . 9 |- (((((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>.)) /\ n e. (H` <.a, A>.)) -> ((GRF)Rn) = (GR(FRn)))
41		simpr 350	. . . . . . . . . . . . 13 |- (((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) /\ (GR(FRm)) = (GR(FRn))) -> (GR(FRm)) = (GR(FRn)))
42		simpll 448	. . . . . . . . . . . . 13 |- (((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) /\ (GR(FRm)) = (GR(FRn))) -> ((GRF)Rm) = (GR(FRm)))
43		simplr 449	. . . . . . . . . . . . 13 |- (((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) /\ (GR(FRm)) = (GR(FRn))) -> ((GRF)Rn) = (GR(FRn)))
44	41, 42, 43	3eqtr4d 1937	. . . . . . . . . . . 12 |- (((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) /\ (GR(FRm)) = (GR(FRn))) -> ((GRF)Rm) = ((GRF)Rn))
45	44	ex 402	. . . . . . . . . . 11 |- ((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) -> ((GR(FRm)) = (GR(FRn)) -> ((GRF)Rm) = ((GRF)Rn)))
46	45	imim1d 33	. . . . . . . . . 10 |- ((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) -> ((((GRF)Rm) = ((GRF)Rn) -> m = n) -> ((GR(FRm)) = (GR(FRn)) -> m = n)))
47		opreq2 4890	. . . . . . . . . 10 |- ((FRm) = (FRn) -> (GR(FRm)) = (GR(FRn)))
48	46, 47	syl7 26	. . . . . . . . 9 |- ((((GRF)Rm) = (GR(FRm)) /\ ((GRF)Rn) = (GR(FRn))) -> ((((GRF)Rm) = ((GRF)Rn) -> m = n) -> ((FRm) = (FRn) -> m = n)))
49	24, 40, 48	syl11anc 524	. . . . . . . 8 |- (((((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>.)) /\ n e. (H` <.a, A>.)) -> ((((GRF)Rm) = ((GRF)Rn) -> m = n) -> ((FRm) = (FRn) -> m = n)))
50	49	ralimdvaa 2171	. . . . . . 7 |- ((((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>.)) -> (A.n e. (H` <.a, A>.)(((GRF)Rm) = ((GRF)Rn) -> m = n) -> A.n e. (H` <.a, A>.)((FRm) = (FRn) -> m = n)))
51	50	ralimdvaa 2171	. . . . . 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) -> (A.m e. (H` <.a, A>.)A.n e. (H` <.a, A>.)(((GRF)Rm) = ((GRF)Rn) -> m = n) -> A.m e. (H` <.a, A>.)A.n e. (H` <.a, A>.)((FRm) = (FRn) -> m = n)))
52	51	ralimdvaa 2171	. . . . 5 |- ((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.m e. (H` <.a, A>.)A.n e. (H` <.a, A>.)(((GRF)Rm) = ((GRF)Rn) -> m = n) -> A.a e. O A.m e. (H` <.a, A>.)A.n e. (H` <.a, A>.)((FRm) = (FRn) -> m = n)))
53	10, 52	sylbid 220	. . . 4 |- ((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>.)((FRm) = (FRn) -> m = n)))
54	53	3exp 1066	. . 3 |- (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>.)((FRm) = (FRn) -> m = n)))))
55	54	3imp2 1083	. 2 |- ((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>.)((FRm) = (FRn) -> m = n))
56		simpl 346	. . 3 |- ((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))) -> T e. Cat )
57		3simpa 872	. . . . 5 |- ((A e. O /\ B e. O /\ C e. O) -> (A e. O /\ B e. O))
58	57	3ad2ant1 897	. . . 4 |- (((A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) /\ (GRF) e. ( Monic ` T)) -> (A e. O /\ B e. O))
59	58	adantl 424	. . 3 |- ((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 e. O /\ B e. O))
60		simpr2l 935	. . 3 |- ((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. (H` <.A, B>.))
61	4, 5, 6	ismonc 15163	. . 3 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ F e. (H` <.A, B>.)) -> (F e. ( Monic ` T) <-> A.a e. O A.m e. (H` <.a, A>.)A.n e. (H` <.a, A>.)((FRm) = (FRn) -> m = n)))
62	56, 59, 60, 61	syl111anc 1100	. 2 |- ((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) <-> A.a e. O A.m e. (H` <.a, A>.)A.n e. (H` <.a, A>.)((FRm) = (FRn) -> m = n)))
63	55, 62	mpbird 213	1 |- ((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))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  <.cop 3046  dom cdm 3986  ` cfv 3998  (class class class)co 4884  idcid_ 15061  oco_ 15062   Cat ccat 15099   hom chom 15134   Monic cmon 15153

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-alg 15063  df-doma 15064  df-coda 15065  df-ida 15066  df-cmpa 15067  df-ded 15082  df-cat 15100  df-hom 15135  df-mon 15155

Copyright terms: Public domain