Theorem ecopoprtrn 4295

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 3224	. . . . . . 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 2081	. . . . . 6 |- R (_ ((S X. S) X. (S X. S))
5	1, 4	brel 3213	. . . . 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 3213	. . . 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 777	. . 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 1468	. . 3 |- (S X. S) = (S X. S)
13		breq1 2612	. . . . 5 |- (<.f, g>. = A -> (<.f, g>.R<.h, t>. <-> AR<.h, t>.))
14	13	anbi1d 615	. . . 4 |- (<.f, g>. = A -> ((<.f, g>.R<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (AR<.h, t>. /\ <.h, t>.R<.s, r>.)))
15		breq1 2612	. . . 4 |- (<.f, g>. = A -> (<.f, g>.R<.s, r>. <-> AR<.s, r>.))
16	14, 15	imbi12d 624	. . 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 2613	. . . . 5 |- (<.h, t>. = B -> (AR<.h, t>. <-> ARB))
18		breq1 2612	. . . . 5 |- (<.h, t>. = B -> (<.h, t>.R<.s, r>. <-> BR<.s, r>.))
19	17, 18	anbi12d 626	. . . 4 |- (<.h, t>. = B -> ((AR<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (ARB /\ BR<.s, r>.)))
20	19	imbi1d 611	. . 3 |- (<.h, t>. = B -> (((AR<.h, t>. /\ <.h, t>.R<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BR<.s, r>.) -> AR<.s, r>.)))
21		breq2 2613	. . . . 5 |- (<.s, r>. = C -> (BR<.s, r>. <-> BRC))
22	21	anbi2d 614	. . . 4 |- (<.s, r>. = C -> ((ARB /\ BR<.s, r>.) <-> (ARB /\ BRC)))
23		breq2 2613	. . . 4 |- (<.s, r>. = C -> (AR<.s, r>. <-> ARC))
24	22, 23	imbi12d 624	. . 3 |- (<.s, r>. = C -> (((ARB /\ BR<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BRC) -> ARC)))
25	2	ecopopreq 4292	. . . . . . . 8 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S)) -> (<.f, g>.R<.h, t>. <-> (fFt) = (gFh)))
26	25	3adant3 797	. . . . . . 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 4292	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (<.h, t>.R<.s, r>. <-> (hFr) = (tFs)))
28	27	3adant1 795	. . . . . . 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 626	. . . . . 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 3955	. . . . . . 7 |- (((fFt) = (gFh) /\ (hFr) = (tFs)) -> ((fFt)F(hFr)) = ((gFh)F(tFs)))
31		visset 1804	. . . . . . . 8 |- h e. V
32		visset 1804	. . . . . . . 8 |- t e. V
33		visset 1804	. . . . . . . 8 |- f e. V
34		ecopopr.com	. . . . . . . 8 |- (xFy) = (yFx)
35		ecopopr.ass	. . . . . . . 8 |- ((xFy)Fz) = (xF(yFz))
36		visset 1804	. . . . . . . 8 |- r e. V
37	31, 32, 33, 34, 35, 36	caopr411 4051	. . . . . . 7 |- ((hFt)F(fFr)) = ((fFt)F(hFr))
38		visset 1804	. . . . . . . . 9 |- g e. V
39		visset 1804	. . . . . . . . 9 |- s e. V
40	38, 32, 31, 34, 35, 39	caopr411 4051	. . . . . . . 8 |- ((gFt)F(hFs)) = ((hFt)F(gFs))
41	38, 32, 31, 34, 35, 39	caopr4 4050	. . . . . . . 8 |- ((gFt)F(hFs)) = ((gFh)F(tFs))
42	40, 41	eqtr3 1489	. . . . . . 7 |- ((hFt)F(gFs)) = ((gFh)F(tFs))
43	30, 37, 42	3eqtr4g 1523	. . . . . 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 3968	. . . . . . . . . . 11 |- (gFs) e. V
46		ecopopr.can	. . . . . . . . . . 11 |- ((x e. S /\ y e. S) -> ((xFy) = (xFz) -> y = z))
47	45, 46	caoprcan 4041	. . . . . . . . . 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 4038	. . . . . . . . . 10 |- ((h e. S /\ t e. S) -> (hFt) e. S)
50	48	caoprcl 4038	. . . . . . . . . 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 827	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ f e. S /\ r e. S) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr