Theorem ecopoprtrn 4301

Description: Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation R, specified by the first hypothesis, is transitive.

Hypotheses

Ref	Expression
ecopopr.1	|- R = {<.x, y>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (zFu) = (wFv)))}
ecopopr.com	|- (xFy) = (yFx)
ecopopr.cl	|- ((x e. S /\ y e. S) -> (xFy) e. S)
ecopopr.ass	|- ((xFy)Fz) = (xF(yFz))
ecopopr.can	|- ((x e. S /\ y e. S) -> ((xFy) = (xFz) -> y = z))
ecopopr.3	|- B e. V
ecopopr.4	|- C e. V

Assertion

Ref	Expression
ecopoprtrn	|- ((ARB /\ BRC) -> ARC)

Distinct variable groups:   x,y,z,w,v,u,F   x,S,y,z,w,v,u

Proof of Theorem ecopoprtrn

Step	Hyp	Ref	Expression
1		ecopopr.3	. . . . . 6 |- B e. V
2		ecopopr.1	. . . . . . 7 |- R = {<.x, y>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (zFu) = (wFv)))}
3		opabssxp 3229	. . . . . . 7 |- {<.x, y>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (zFu) = (wFv)))} (_ ((S X. S) X. (S X. S))
4	2, 3	eqsstr 2087	. . . . . 6 |- R (_ ((S X. S) X. (S X. S))
5	1, 4	brel 3218	. . . . 5 |- (ARB -> (A e. (S X. S) /\ B e. (S X. S)))
6	5	pm3.26d 321	. . . 4 |- (ARB -> A e. (S X. S))
7		ecopopr.4	. . . . 5 |- C e. V
8	7, 4	brel 3218	. . . 4 |- (BRC -> (B e. (S X. S) /\ C e. (S X. S)))
9	6, 8	anim12i 333	. . 3 |- ((ARB /\ BRC) -> (A e. (S X. S) /\ (B e. (S X. S) /\ C e. (S X. S))))
10		3anass 778	. . 3 |- ((A e. (S X. S) /\ B e. (S X. S) /\ C e. (S X. S)) <-> (A e. (S X. S) /\ (B e. (S X. S) /\ C e. (S X. S))))
11	9, 10	sylibr 200	. 2 |- ((ARB /\ BRC) -> (A e. (S X. S) /\ B e. (S X. S) /\ C e. (S X. S)))
12		eqid 1473	. . 3 |- (S X. S) = (S X. S)
13		breq1 2617	. . . . 5 |- (<.f, g>. = A -> (<.f, g>.R<.h, t>. <-> AR<.h, t>.))
14	13	anbi1d 616	. . . 4 |- (<.f, g>. = A -> ((<.f, g>.R<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (AR<.h, t>. /\ <.h, t>.R<.s, r>.)))
15		breq1 2617	. . . 4 |- (<.f, g>. = A -> (<.f, g>.R<.s, r>. <-> AR<.s, r>.))
16	14, 15	imbi12d 625	. . 3 |- (<.f, g>. = A -> (((<.f, g>.R<.h, t>. /\ <.h, t>.R<.s, r>.) -> <.f, g>.R<.s, r>.) <-> ((AR<.h, t>. /\ <.h, t>.R<.s, r>.) -> AR<.s, r>.)))
17		breq2 2618	. . . . 5 |- (<.h, t>. = B -> (AR<.h, t>. <-> ARB))
18		breq1 2617	. . . . 5 |- (<.h, t>. = B -> (<.h, t>.R<.s, r>. <-> BR<.s, r>.))
19	17, 18	anbi12d 627	. . . 4 |- (<.h, t>. = B -> ((AR<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (ARB /\ BR<.s, r>.)))
20	19	imbi1d 612	. . 3 |- (<.h, t>. = B -> (((AR<.h, t>. /\ <.h, t>.R<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BR<.s, r>.) -> AR<.s, r>.)))
21		breq2 2618	. . . . 5 |- (<.s, r>. = C -> (BR<.s, r>. <-> BRC))
22	21	anbi2d 615	. . . 4 |- (<.s, r>. = C -> ((ARB /\ BR<.s, r>.) <-> (ARB /\ BRC)))
23		breq2 2618	. . . 4 |- (<.s, r>. = C -> (AR<.s, r>. <-> ARC))
24	22, 23	imbi12d 625	. . 3 |- (<.s, r>. = C -> (((ARB /\ BR<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BRC) -> ARC)))
25	2	ecopopreq 4298	. . . . . . . 8 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S)) -> (<.f, g>.R<.h, t>. <-> (fFt) = (gFh)))
26	25	3adant3 798	. . . . . . 7 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (<.f, g>.R<.h, t>. <-> (fFt) = (gFh)))
27	2	ecopopreq 4298	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (<.h, t>.R<.s, r>. <-> (hFr) = (tFs)))
28	27	3adant1 796	. . . . . . 7 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (<.h, t>.R<.s, r>. <-> (hFr) = (tFs)))
29	26, 28	anbi12d 627	. . . . . 6 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> ((<.f, g>.R<.h, t>. /\ <.h, t>.R<.s, r>.) <-> ((fFt) = (gFh) /\ (hFr) = (tFs))))
30		opreq12 3961	. . . . . . 7 |- (((fFt) = (gFh) /\ (hFr) = (tFs)) -> ((fFt)F(hFr)) = ((gFh)F(tFs)))
31		visset 1809	. . . . . . . 8 |- h e. V
32		visset 1809	. . . . . . . 8 |- t e. V
33		visset 1809	. . . . . . . 8 |- f e. V
34		ecopopr.com	. . . . . . . 8 |- (xFy) = (yFx)
35		ecopopr.ass	. . . . . . . 8 |- ((xFy)Fz) = (xF(yFz))
36		visset 1809	. . . . . . . 8 |- r e. V
37	31, 32, 33, 34, 35, 36	caopr411 4057	. . . . . . 7 |- ((hFt)F(fFr)) = ((fFt)F(hFr))
38		visset 1809	. . . . . . . . 9 |- g e. V
39		visset 1809	. . . . . . . . 9 |- s e. V
40	38, 32, 31, 34, 35, 39	caopr411 4057	. . . . . . . 8 |- ((gFt)F(hFs)) = ((hFt)F(gFs))
41	38, 32, 31, 34, 35, 39	caopr4 4056	. . . . . . . 8 |- ((gFt)F(hFs)) = ((gFh)F(tFs))
42	40, 41	eqtr3 1494	. . . . . . 7 |- ((hFt)F(gFs)) = ((gFh)F(tFs))
43	30, 37, 42	3eqtr4g 1528	. . . . . 6 |- (((fFt) = (gFh) /\ (hFr) = (tFs)) -> ((hFt)F(fFr)) = ((hFt)F(gFs)))
44	29, 43	syl6bi 214	. . . . 5 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> ((<.f, g>.R<.h, t>. /\ <.h, t>.R<.s, r>.) -> ((hFt)F(fFr)) = ((hFt)F(gFs))))
45		oprex 3974	. . . . . . . . . . 11 |- (gFs) e. V
46		ecopopr.can	. . . . . . . . . . 11 |- ((x e. S /\ y e. S) -> ((xFy) = (xFz) -> y = z))
47	45, 46	caoprcan 4047	. . . . . . . . . 10 |- (((hFt) e. S /\ (fFr) e. S) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
48		ecopopr.cl	. . . . . . . . . . 11 |- ((x e. S /\ y e. S) -> (xFy) e. S)
49	48	caoprcl 4044	. . . . . . . . . 10 |- ((h e. S /\ t e. S) -> (hFt) e. S)
50	48	caoprcl 4044	. . . . . . . . . 10 |- ((f e. S /\ r e. S) -> (fFr) e. S)
51	47, 49, 50	syl2an 454	. . . . . . . . 9 |- (((h e. S /\ t e. S) /\ (f e. S /\ r e. S)) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
52	51	3impb 828	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ f e. S /\ r e. S) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr