Theorem ecopoprtrn 4311

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 3234	. . . . . . 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 2091	. . . . . 6 |- R (_ ((S X. S) X. (S X. S))
5	1, 4	brel 3223	. . . . 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 3223	. . . 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 779	. . 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 1475	. . 3 |- (S X. S) = (S X. S)
13		breq1 2622	. . . . 5 |- (<.f, g>. = A -> (<.f, g>.R<.h, t>. <-> AR<.h, t>.))
14	13	anbi1d 617	. . . 4 |- (<.f, g>. = A -> ((<.f, g>.R<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (AR<.h, t>. /\ <.h, t>.R<.s, r>.)))
15		breq1 2622	. . . 4 |- (<.f, g>. = A -> (<.f, g>.R<.s, r>. <-> AR<.s, r>.))
16	14, 15	imbi12d 626	. . 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 2623	. . . . 5 |- (<.h, t>. = B -> (AR<.h, t>. <-> ARB))
18		breq1 2622	. . . . 5 |- (<.h, t>. = B -> (<.h, t>.R<.s, r>. <-> BR<.s, r>.))
19	17, 18	anbi12d 628	. . . 4 |- (<.h, t>. = B -> ((AR<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (ARB /\ BR<.s, r>.)))
20	19	imbi1d 613	. . 3 |- (<.h, t>. = B -> (((AR<.h, t>. /\ <.h, t>.R<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BR<.s, r>.) -> AR<.s, r>.)))
21		breq2 2623	. . . . 5 |- (<.s, r>. = C -> (BR<.s, r>. <-> BRC))
22	21	anbi2d 616	. . . 4 |- (<.s, r>. = C -> ((ARB /\ BR<.s, r>.) <-> (ARB /\ BRC)))
23		breq2 2623	. . . 4 |- (<.s, r>. = C -> (AR<.s, r>. <-> ARC))
24	22, 23	imbi12d 626	. . 3 |- (<.s, r>. = C -> (((ARB /\ BR<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BRC) -> ARC)))
25	2	ecopopreq 4308	. . . . . . . 8 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S)) -> (<.f, g>.R<.h, t>. <-> (fFt) = (gFh)))
26	25	3adant3 799	. . . . . . 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 4308	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (<.h, t>.R<.s, r>. <-> (hFr) = (tFs)))
28	27	3adant1 797	. . . . . . 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 628	. . . . . 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 3970	. . . . . . 7 |- (((fFt) = (gFh) /\ (hFr) = (tFs)) -> ((fFt)F(hFr)) = ((gFh)F(tFs)))
31		visset 1813	. . . . . . . 8 |- h e. V
32		visset 1813	. . . . . . . 8 |- t e. V
33		visset 1813	. . . . . . . 8 |- f e. V
34		ecopopr.com	. . . . . . . 8 |- (xFy) = (yFx)
35		ecopopr.ass	. . . . . . . 8 |- ((xFy)Fz) = (xF(yFz))
36		visset 1813	. . . . . . . 8 |- r e. V
37	31, 32, 33, 34, 35, 36	caopr411 4065	. . . . . . 7 |- ((hFt)F(fFr)) = ((fFt)F(hFr))
38		visset 1813	. . . . . . . . 9 |- g e. V
39		visset 1813	. . . . . . . . 9 |- s e. V
40	38, 32, 31, 34, 35, 39	caopr411 4065	. . . . . . . 8 |- ((gFt)F(hFs)) = ((hFt)F(gFs))
41	38, 32, 31, 34, 35, 39	caopr4 4064	. . . . . . . 8 |- ((gFt)F(hFs)) = ((gFh)F(tFs))
42	40, 41	eqtr3 1497	. . . . . . 7 |- ((hFt)F(gFs)) = ((gFh)F(tFs))
43	30, 37, 42	3eqtr4g 1531	. . . . . 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 3983	. . . . . . . . . . 11 |- (gFs) e. V
46		ecopopr.can	. . . . . . . . . . 11 |- ((x e. S /\ y e. S) -> ((xFy) = (xFz) -> y = z))
47	45, 46	caoprcan 4055	. . . . . . . . . 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 4052	. . . . . . . . . 10 |- ((h e. S /\ t e. S) -> (hFt) e. S)
50	48	caoprcl 4052	. . . . . . . . . 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 829	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ f e. S /\ r e. S) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fF