Theorem cmpmon 15164

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 1317	. . . . . . . 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 2147	. . . . . . . . 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 2147	. . . . . . . . 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 1356	. . . . . . . 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 1356	. . . . . . 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 1317	. . . . . . . . . . 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 1317	. . . . . . . . . . . . 13 |- (a e. O -> A.g a e. O)
8		hbra1 2147	. . . . . . . . . . . . 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 2146	. . . . . . . . . . . 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 1317	. . . . . . . . . . . 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 1356	. . . . . . . . . . 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 1356	. . . . . . . . . 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 1356	. . . . . . . . 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 1317	. . . . . . . . . . . . . 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 1317	. . . . . . . . . . . . . . . 16 |- (a e. O -> A.h a e. O)
16		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- (g e. (H` <.a, A>.) -> A.h g e. (H` <.a, A>.))
17		hbra1 2147	. . . . . . . . . . . . . . . . 17 |- (A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) -> A.hA.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h))
18	16, 17	hbral 2146	. . . . . . . . . . . . . . . 16 |- (A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) -> A.hA.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h))
19	15, 18	hbral 2146	. . . . . . . . . . . . . . 15 |- (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) -> A.hA.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h))
20		ax-17 1317	. . . . . . . . . . . . . . 15 |- (A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l) -> A.hA.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))
21	19, 20	hban 1356	. . . . . . . . . . . . . 14 |- ((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.h(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)))
22	14, 21	hban 1356	. . . . . . . . . . . . 13 |- (((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.h((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))))
23	22, 15	hban 1356	. . . . . . . . . . . 12 |- ((((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.h(((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))
24	23, 16	hban 1356	. . . . . . . . . . 11 |- (((((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) /\ g e. (H` <.a, A>.)) -> A.h((((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) /\ g e. (H` <.a, A>.)))
25		cmpmon.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- O = dom (id` T)
26		cmpmon.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- H = ( hom ` T)
27		cmpmon.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- R = (o` T)
28	25, 26, 27	cmpassoh 15150	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((T e. Cat /\ (a e. O /\ A e. O) /\ (B e. O /\ C e. O)) -> ((g e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRg)) = ((GRF)Rg)))
29	28	3expib 1070	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (T e. Cat -> (((a e. O /\ A e. O) /\ (B e. O /\ C e. O)) -> ((g e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRg)) = ((GRF)Rg))))
30	29	com3r 39	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((g e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (T e. Cat -> (((a e. O /\ A e. O) /\ (B e. O /\ C e. O)) -> (GR(FRg)) = ((GRF)Rg))))
31	30	3expib 1070	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (g e. (H` <.a, A>.) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (T e. Cat -> (((a e. O /\ A e. O) /\ (B e. O /\ C e. O)) -> (GR(FRg)) = ((GRF)Rg)))))
32	31	com23 36	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (g e. (H` <.a, A>.) -> (T e. Cat -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (((a e. O /\ A e. O) /\ (B e. O /\ C e. O)) -> (GR(FRg)) = ((GRF)Rg)))))
33	32	com14 42	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((a e. O /\ A e. O) /\ (B e. O /\ C e. O)) -> (T e. Cat -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (g e. (H` <.a, A>.) -> (GR(FRg)) = ((GRF)Rg)))))
34	33	exp43 415	. . . . . . . . . . . . . . . . . . . . . 22 |- (a e. O -> (A e. O -> (B e. O -> (C e. O -> (T e. Cat -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (g e. (H` <.a, A>.) -> (GR(FRg)) = ((GRF)Rg))))))))
35	34	3impd 1082	. . . . . . . . . . . . . . . . . . . . 21 |- (a e. O -> ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (g e. (H` <.a, A>.) -> (GR(FRg)) = ((GRF)Rg))))))
36	35	com13 37	. . . . . . . . . . . . . . . . . . . 20 |- (T e. Cat -> ((A e. O /\ B e. O /\ C e. O) -> (a e. O -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (g e. (H` <.a, A>.) -> (GR(FRg)) = ((GRF)Rg))))))
37	36	com34 40	. . . . . . . . . . . . . . . . . . 19 |- (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 -> (g e. (H` <.a, A>.) -> (GR(FRg)) = ((GRF)Rg))))))
38	37	3imp 1061	. . . . . . . . . . . . . . . . . 18 |- ((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 -> (g e. (H` <.a, A>.) -> (GR(FRg)) = ((GRF)Rg))))
39	38	adantr 425	. . . . . . . . . . . . . . . . 17 |- (((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 -> (g e. (H` <.a, A>.) -> (GR(FRg)) = ((GRF)Rg))))
40	39	imp31 389	. . . . . . . . . . . . . . . 16 |- (((((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) /\ g e. (H` <.a, A>.)) -> (GR(FRg)) = ((GRF)Rg))
41	40	ad2antrr 440	. . . . . . . . . . . . . . 15 |- (((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) /\ ((GRF)Rg) = ((GRF)Rh)) -> (GR(FRg)) = ((GRF)Rg))
42		eqcom 1886	. . . . . . . . . . . . . . . . 17 |- (((GRF)Rg) = ((GRF)Rh) <-> ((GRF)Rh) = ((GRF)Rg))
43	42	biimpi 168	. . . . . . . . . . . . . . . 16 |- (((GRF)Rg) = ((GRF)Rh) -> ((GRF)Rh) = ((GRF)Rg))
44	43	adantl 424	. . . . . . . . . . . . . . 15 |- (((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) /\ ((GRF)Rg) = ((GRF)Rh)) -> ((GRF)Rh) = ((GRF)Rg))
45	25, 26, 27	cmpassoh 15150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((T e. Cat /\ (a e. O /\ A e. O) /\ (B e. O /\ C e. O)) -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (GR(FRh)) = ((GRF)Rh)))
46	45	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((T e. Cat /\ (a e. O /\ A e. O) /\ (B e. O /\ C e. O)) /\ (h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> (GR(FRh)) = ((GRF)Rh))
47	46	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((T e. Cat /\ (a e. O /\ A e. O) /\ (B e. O /\ C e. O)) /\ (h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> ((GRF)Rh) = (GR(FRh)))
48	47	3exp1 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (T e. Cat -> ((a e. O /\ A e. O) -> ((B e. O /\ C e. O) -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh))))))
49	48	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((a e. O /\ A e. O) -> ((B e. O /\ C e. O) -> (T e. Cat -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh))))))
50	49	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (a e. O -> (A e. O -> ((B e. O /\ C e. O) -> (T e. Cat -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh)))))))
51	50	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (a e. O -> ((B e. O /\ C e. O) -> (A e. O -> (T e. Cat -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh)))))))
52	51	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (T e. Cat -> ((B e. O /\ C e. O) -> (A e. O -> (a e. O -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh)))))))
53	52	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((B e. O /\ C e. O) -> (T e. Cat -> (A e. O -> (a e. O -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh)))))))
54	53	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (B e. O -> (C e. O -> (T e. Cat -> (A e. O -> (a e. O -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh))))))))
55	54	com4r 45	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A e. O -> (B e. O -> (C e. O -> (T e. Cat -> (a e. O -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh))))))))
56	55	3imp 1061	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> (a e. O -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh))))))
57	56	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O)) -> (a e. O -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((GRF)Rh) = (GR(FRh)))))
58	57	com13 37	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((h 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)) -> ((GRF)Rh) = (GR(FRh)))))
59	58	3expib 1070	. . . . . . . . . . . . . . . . . . . . . 22 |- (h 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)) -> ((GRF)Rh) = (GR(FRh))))))
60	59	com14 42	. . . . . . . . . . . . . . . . . . . . 21 |- ((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 -> (h e. (H` <.a, A>.) -> ((GRF)Rh) = (GR(FRh))))))
61	60	3impia 1064	. . . . . . . . . . . . . . . . . . . 20 |- ((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 -> (h e. (H` <.a, A>.) -> ((GRF)Rh) = (GR(FRh)))))
62	61	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- (((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 -> (h e. (H` <.a, A>.) -> ((GRF)Rh) = (GR(FRh)))))
63	62	imp 377	. . . . . . . . . . . . . . . . . 18 |- ((((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) -> (h e. (H` <.a, A>.) -> ((GRF)Rh) = (GR(FRh))))
64	63	adantr 425	. . . . . . . . . . . . . . . . 17 |- (((((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) /\ g e. (H` <.a, A>.)) -> (h e. (H` <.a, A>.) -> ((GRF)Rh) = (GR(FRh))))
65	64	imp 377	. . . . . . . . . . . . . . . 16 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> ((GRF)Rh) = (GR(FRh)))
66	65	adantr 425	. . . . . . . . . . . . . . 15 |- (((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) /\ ((GRF)Rg) = ((GRF)Rh)) -> ((GRF)Rh) = (GR(FRh)))
67	41, 44, 66	3eqtr2d 1932	. . . . . . . . . . . . . 14 |- (((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) /\ ((GRF)Rg) = ((GRF)Rh)) -> (GR(FRg)) = (GR(FRh)))
68	67	ex 402	. . . . . . . . . . . . 13 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> (((GRF)Rg) = ((GRF)Rh) -> (GR(FRg)) = (GR(FRh))))
69	25, 26, 27	homgrf 15151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((T e. Cat /\ (a e. O /\ A e. O /\ B e. O)) -> ((g e. (H` <.a, A>.) /\ F e. (H` <.A, B>.)) -> (FRg) e. (H` <.a, B>.)))
70	69	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (T e. Cat -> ((a e. O /\ A e. O /\ B e. O) -> ((g e. (H` <.a, A>.) /\ F e. (H` <.A, B>.)) -> (FRg) e. (H` <.a, B>.))))
71	70	com3r 39	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((g e. (H` <.a, A>.) /\ F e. (H` <.A, B>.)) -> (T e. Cat -> ((a e. O /\ A e. O /\ B e. O) -> (FRg) e. (H` <.a, B>.))))
72	71	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (g e. (H` <.a, A>.) -> (F e. (H` <.A, B>.) -> (T e. Cat -> ((a e. O /\ A e. O /\ B e. O) -> (FRg) e. (H` <.a, B>.)))))
73	72	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (g e. (H` <.a, A>.) -> (T e. Cat -> (F e. (H` <.A, B>.) -> ((a e. O /\ A e. O /\ B e. O) -> (FRg) e. (H` <.a, B>.)))))
74	73	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((a e. O /\ A e. O /\ B e. O) -> (T e. Cat -> (F e. (H` <.A, B>.) -> (g e. (H` <.a, A>.) -> (FRg) e. (H` <.a, B>.)))))
75	74	3expib 1070	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (a e. O -> ((A e. O /\ B e. O) -> (T e. Cat -> (F e. (H` <.A, B>.) -> (g e. (H` <.a, A>.) -> (FRg) e. (H` <.a, B>.))))))
76	75	com14 42	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F e. (H` <.A, B>.) -> ((A e. O /\ B e. O) -> (T e. Cat -> (a e. O -> (g e. (H` <.a, A>.) -> (FRg) e. (H` <.a, B>.))))))
77		3simpa 872	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. O /\ B e. O /\ C e. O) -> (A e. O /\ B e. O))
78	76, 77	syl5 20	. . . . . . . . . . . . . . . . . . . . . 22 |- (F e. (H` <.A, B>.) -> ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> (a e. O -> (g e. (H` <.a, A>.) -> (FRg) e. (H` <.a, B>.))))))
79	78	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- ((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 -> (g e. (H` <.a, A>.) -> (FRg) e. (H` <.a, B>.))))))
80	79	com13 37	. . . . . . . . . . . . . . . . . . . 20 |- (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 -> (g e. (H` <.a, A>.) -> (FRg) e. (H` <.a, B>.))))))
81	80	3imp 1061	. . . . . . . . . . . . . . . . . . 19 |- ((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 -> (g e. (H` <.a, A>.) -> (FRg) e. (H` <.a, B>.))))
82	81	adantr 425	. . . . . . . . . . . . . . . . . 18 |- (((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 -> (g e. (H` <.a, A>.) -> (FRg) e. (H` <.a, B>.))))
83	82	imp31 389	. . . . . . . . . . . . . . . . 17 |- (((((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) /\ g e. (H` <.a, A>.)) -> (FRg) e. (H` <.a, B>.))
84	83	adantr 425	. . . . . . . . . . . . . . . 16 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> (FRg) e. (H` <.a, B>.))
85	25, 26, 27	homgrf 15151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((T e. Cat /\ (a e. O /\ A e. O /\ B e. O)) -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.)) -> (FRh) e. (H` <.a, B>.)))
86	85	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (T e. Cat -> ((a e. O /\ A e. O /\ B e. O) -> ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.)) -> (FRh) e. (H` <.a, B>.))))
87	86	com3r 39	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((h e. (H` <.a, A>.) /\ F e. (H` <.A, B>.)) -> (T e. Cat -> ((a e. O /\ A e. O /\ B e. O) -> (FRh) e. (H` <.a, B>.))))
88	87	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (h e. (H` <.a, A>.) -> (F e. (H` <.A, B>.) -> (T e. Cat -> ((a e. O /\ A e. O /\ B e. O) -> (FRh) e. (H` <.a, B>.)))))
89	88	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((a e. O /\ A e. O /\ B e. O) -> (F e. (H` <.A, B>.) -> (T e. Cat -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.)))))
90	89	adantrd 427	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((a e. O /\ A e. O /\ B e. O) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (T e. Cat -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.)))))
91	90	3expib 1070	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a e. O -> ((A e. O /\ B e. O) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (T e. Cat -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.))))))
92	91	com12 14	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. O /\ B e. O) -> (a e. O -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (T e. Cat -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.))))))
93	92	com24 41	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. O /\ B e. O) -> (T e. Cat -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (a e. O -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.))))))
94	93	3adant3 896	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (a e. O -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.))))))
95	94	com12 14	. . . . . . . . . . . . . . . . . . . . 21 |- (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 -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.))))))
96	95	3imp 1061	. . . . . . . . . . . . . . . . . . . 20 |- ((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 -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.))))
97	96	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- (((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 -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.))))
98	97	imp 377	. . . . . . . . . . . . . . . . . 18 |- ((((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) -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.)))
99	98	adantr 425	. . . . . . . . . . . . . . . . 17 |- (((((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) /\ g e. (H` <.a, A>.)) -> (h e. (H` <.a, A>.) -> (FRh) e. (H` <.a, B>.)))
100	99	imp 377	. . . . . . . . . . . . . . . 16 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> (FRh) e. (H` <.a, B>.))
101	84, 100	jca 310	. . . . . . . . . . . . . . 15 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> ((FRg) e. (H` <.a, B>.) /\ (FRh) e. (H` <.a, B>.)))
102		ra4 2155	. . . . . . . . . . . . . . . . . 18 |- (A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l) -> (a e. O -> A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))
103	102	ad2antll 443	. . . . . . . . . . . . . . . . 17 |- (((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.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))
104	103	imp 377	. . . . . . . . . . . . . . . 16 |- ((((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.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))
105	104	ad2antrr 440	. . . . . . . . . . . . . . 15 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l))
106		opreq2 4890	. . . . . . . . . . . . . . . . . 18 |- (k = (FRg) -> (GRk) = (GR(FRg)))
107	106	eqeq1d 1892	. . . . . . . . . . . . . . . . 17 |- (k = (FRg) -> ((GRk) = (GRl) <-> (GR(FRg)) = (GRl)))
108		eqeq1 1890	. . . . . . . . . . . . . . . . 17 |- (k = (FRg) -> (k = l <-> (FRg) = l))
109	107, 108	imbi12d 688	. . . . . . . . . . . . . . . 16 |- (k = (FRg) -> (((GRk) = (GRl) -> k = l) <-> ((GR(FRg)) = (GRl) -> (FRg) = l)))
110		opreq2 4890	. . . . . . . . . . . . . . . . . 18 |- (l = (FRh) -> (GRl) = (GR(FRh)))
111	110	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (l = (FRh) -> ((GR(FRg)) = (GRl) <-> (GR(FRg)) = (GR(FRh))))
112		eqeq2 1893	. . . . . . . . . . . . . . . . 17 |- (l = (FRh) -> ((FRg) = l <-> (FRg) = (FRh)))
113	111, 112	imbi12d 688	. . . . . . . . . . . . . . . 16 |- (l = (FRh) -> (((GR(FRg)) = (GRl) -> (FRg) = l) <-> ((GR(FRg)) = (GR(FRh)) -> (FRg) = (FRh))))
114	109, 113	rcla42v 2384	. . . . . . . . . . . . . . 15 |- (((FRg) e. (H` <.a, B>.) /\ (FRh) e. (H` <.a, B>.)) -> (A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l) -> ((GR(FRg)) = (GR(FRh)) -> (FRg) = (FRh))))
115	101, 105, 114	sylc 83	. . . . . . . . . . . . . 14 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> ((GR(FRg)) = (GR(FRh)) -> (FRg) = (FRh)))
116		r3al 2151	. . . . . . . . . . . . . . . . . . . 20 |- (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) <-> A.aA.gA.h((a e. O /\ g e. (H` <.a, A>.) /\ h e. (H` <.a, A>.)) -> ((FRg) = (FRh) -> g = h)))
117	116	biimpi 168	. . . . . . . . . . . . . . . . . . 19 |- (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) -> A.aA.gA.h((a e. O /\ g e. (H` <.a, A>.) /\ h e. (H` <.a, A>.)) -> ((FRg) = (FRh) -> g = h)))
118	117	19.21bi 1408	. . . . . . . . . . . . . . . . . 18 |- (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) -> A.gA.h((a e. O /\ g e. (H` <.a, A>.) /\ h e. (H` <.a, A>.)) -> ((FRg) = (FRh) -> g = h)))
119	118	19.21bbi 1409	. . . . . . . . . . . . . . . . 17 |- (A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h) -> ((a e. O /\ g e. (H` <.a, A>.) /\ h e. (H` <.a, A>.)) -> ((FRg) = (FRh) -> g = h)))
120	119	ad2antrl 442	. . . . . . . . . . . . . . . 16 |- (((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 /\ g e. (H` <.a, A>.) /\ h e. (H` <.a, A>.)) -> ((FRg) = (FRh) -> g = h)))
121	120	3expd 1085	. . . . . . . . . . . . . . 15 |- (((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 -> (g e. (H` <.a, A>.) -> (h e. (H` <.a, A>.) -> ((FRg) = (FRh) -> g = h)))))
122	121	imp41 395	. . . . . . . . . . . . . 14 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> ((FRg) = (FRh) -> g = h))
123	115, 122	syld 30	. . . . . . . . . . . . 13 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> ((GR(FRg)) = (GR(FRh)) -> g = h))
124	68, 123	syld 30	. . . . . . . . . . . 12 |- ((((((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) /\ g e. (H` <.a, A>.)) /\ h e. (H` <.a, A>.)) -> (((GRF)Rg) = ((GRF)Rh) -> g = h))
125	124	ex 402	. . . . . . . . . . 11 |- (((((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) /\ g e. (H` <.a, A>.)) -> (h e. (H` <.a, A>.) -> (((GRF)Rg) = ((GRF)Rh) -> g = h)))
126	24, 125	r19.21ai 2174	. . . . . . . . . 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 e. O) /\ g e. (H` <.a, A>.)) -> A.h e. (H` <.a, A>.)(((GRF)Rg) = ((GRF)Rh) -> g = h))
127	126	ex 402	. . . . . . . . 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) -> (g e. (H` <.a, A>.) -> A.h e. (H` <.a, A>.)(((GRF)Rg) = ((GRF)Rh) -> g = h)))
128	13, 127	r19.21ai 2174	. . . . . . . 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 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 e. (H` <.a, A>.)A.h e. (H` <.a, A>.)(((GRF)Rg) = ((GRF)Rh) -> g = h))
129	128	ex 402	. . . . . . 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 e. O -> A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)(((GRF)Rg) = ((GRF)Rh) -> g = h)))
130	5, 129	r19.21ai 2174	. . . . . 6 |- (((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 e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)(((GRF)Rg) = ((GRF)Rh) -> g = h))
131	130	ex 402	. . . . 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.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 e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)(((GRF)Rg) = ((GRF)Rh) -> g = h)))
132		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 )
133		3simpb 873	. . . . . . 7 |- ((A e. O /\ B e. O /\ C e. O) -> (A e. O /\ C e. O))
134	133	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))
135	25, 26, 27	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>.)))
136	135	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>.))
137	25, 26, 27	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.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)(((GRF)Rg) = ((GRF)Rh) -> g = h)))
138	132, 134, 136, 137	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.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)(((GRF)Rg) = ((GRF)Rh) -> g = h)))
139	131, 138	sylibrd 221	. . . 4 |- ((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)) -> (GRF) e. ( Monic ` T)))
140	25, 26, 27	ismonc 15163	. . . . . . . . . . 11 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ F e. (H` <.A, B>.)) -> (F e. ( Monic ` T) <-> A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h)))
141	140	biimpd 170	. . . . . . . . . 10 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ F e. (H` <.A, B>.)) -> (F e. ( Monic ` T) -> A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h)))
142	141	3exp 1066	. . . . . . . . 9 |- (T e. Cat -> ((A e. O /\ B e. O) -> (F e. (H` <.A, B>.) -> (F e. ( Monic ` T) -> A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h)))))
143	142	com13 37	. . . . . . . 8 |- (F e. (H` <.A, B>.) -> ((A e. O /\ B e. O) -> (T e. Cat -> (F e. ( Monic ` T) -> A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h)))))
144	143	adantr 425	. . . . . . 7 |- ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((A e. O /\ B e. O) -> (T e. Cat -> (F e. ( Monic ` T) -> A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h)))))
145	144	com13 37	. . . . . 6 |- (T e. Cat -> ((A e. O /\ B e. O) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (F e. ( Monic ` T) -> A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h)))))
146	145, 77	syl5 20	. . . . 5 |- (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) -> A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h)))))
147	146	3imp 1061	. . . 4 |- ((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) -> A.a e. O A.g e. (H` <.a, A>.)A.h e. (H` <.a, A>.)((FRg) = (FRh) -> g = h)))
148	25, 26, 27	ismonc 15163	. . . . . . . . . . 11 |- ((T e. Cat /\ (B e. O /\ C e. O) /\ G e. (H` <.B, C>.)) -> (G e. ( Monic ` T) <-> A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))
149	148	biimpd 170	. . . . . . . . . 10 |- ((T e. Cat /\ (B e. O /\ C e. O) /\ G e. (H` <.B, C>.)) -> (G e. ( Monic ` T) -> A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))
150	149	3exp 1066	. . . . . . . . 9 |- (T e. Cat -> ((B e. O /\ C e. O) -> (G e. (H` <.B, C>.) -> (G e. ( Monic ` T) -> A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))))
151	150	com13 37	. . . . . . . 8 |- (G e. (H` <.B, C>.) -> ((B e. O /\ C e. O) -> (T e. Cat -> (G e. ( Monic ` T) -> A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))))
152	151	adantl 424	. . . . . . 7 |- ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> ((B e. O /\ C e. O) -> (T e. Cat -> (G e. ( Monic ` T) -> A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))))
153	152	com13 37	. . . . . 6 |- (T e. Cat -> ((B e. O /\ C e. O) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (G e. ( Monic ` T) -> A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))))
154		3simpc 874	. . . . . 6 |- ((A e. O /\ B e. O /\ C e. O) -> (B e. O /\ C e. O))
155	153, 154	syl5 20	. . . . 5 |- (T e. Cat -> ((A e. O /\ B e. O /\ C e. O) -> ((F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) -> (G e. ( Monic ` T) -> A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))))
156	155	3imp 1061	. . . 4 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.))) -> (G e. ( Monic ` T) -> A.a e. O A.k e. (H` <.a, B>.)A.l e. (H` <.a, B>.)((GRk) = (GRl) -> k = l)))
157	139, 147, 156	syl2and 508	. . 3 |- ((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)))
158	157	3exp 1066	. 2 |- (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)))))
159	158	3imp2 1083	1 |- ((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))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = 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