Theorem ecopoprtrn 3247

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 group(s):   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 2468	. . . . . . 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 1530	. . . . . 6 |- R (_ ((S X. S) X. (S X. S))
5	1, 4	brel 2459	. . . . 5 |- (ARB -> (A e. (S X. S) /\ B e. (S X. S)))
6	5	pm3.26d 258	. . . 4 |- (ARB -> A e. (S X. S))
7		ecopopr.4	. . . . 5 |- C e. V
8	7, 4	brel 2459	. . . 4 |- (BRC -> (B e. (S X. S) /\ C e. (S X. S)))
9	6, 8	anim12i 268	. . 3 |- ((ARB /\ BRC) -> (A e. (S X. S) /\ (B e. (S X. S) /\ C e. (S X. S))))
10		3anass 585	. . 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 175	. 2 |- ((ARB /\ BRC) -> (A e. (S X. S) /\ B e. (S X. S) /\ C e. (S X. S)))
12		cleqid 1102	. . 3 |- (S X. S) = (S X. S)
13		breq1 2065	. . . . 5 |- (<.f, g>. = A -> (<.f, g>.R<.h, t>. <-> AR<.h, t>.))
14	13	anbi1d 469	. . . 4 |- (<.f, g>. = A -> ((<.f, g>.R<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (AR<.h, t>. /\ <.h, t>.R<.s, r>.)))
15		breq1 2065	. . . 4 |- (<.f, g>. = A -> (<.f, g>.R<.s, r>. <-> AR<.s, r>.))
16	14, 15	imbi12d 474	. . 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 2066	. . . . 5 |- (<.h, t>. = B -> (AR<.h, t>. <-> ARB))
18		breq1 2065	. . . . 5 |- (<.h, t>. = B -> (<.h, t>.R<.s, r>. <-> BR<.s, r>.))
19	17, 18	anbi12d 476	. . . 4 |- (<.h, t>. = B -> ((AR<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (ARB /\ BR<.s, r>.)))
20	19	imbi1d 465	. . 3 |- (<.h, t>. = B -> (((AR<.h, t>. /\ <.h, t>.R<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BR<.s, r>.) -> AR<.s, r>.)))
21		breq2 2066	. . . . 5 |- (<.s, r>. = C -> (BR<.s, r>. <-> BRC))
22	21	anbi2d 468	. . . 4 |- (<.s, r>. = C -> ((ARB /\ BR<.s, r>.) <-> (ARB /\ BRC)))
23		breq2 2066	. . . 4 |- (<.s, r>. = C -> (AR<.s, r>. <-> ARC))
24	22, 23	imbi12d 474	. . 3 |- (<.s, r>. = C -> (((ARB /\ BR<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BRC) -> ARC)))
25	2	ecopopreq 3244	. . . . . . . 8 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S)) -> (<.f, g>.R<.h, t>. <-> (fFt) = (gFh)))
26	25	3adant3 599	. . . . . . 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 3244	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (<.h, t>.R<.s, r>. <-> (hFr) = (tFs)))
28	27	3adant1 597	. . . . . . 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 476	. . . . . 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 3008	. . . . . . 7 |- (((fFt) = (gFh) /\ (hFr) = (tFs)) -> ((fFt)F(hFr)) = ((gFh)F(tFs)))
31		visset 1350	. . . . . . . 8 |- h e. V
32		visset 1350	. . . . . . . 8 |- t e. V
33		visset 1350	. . . . . . . 8 |- f e. V
34		ecopopr.com	. . . . . . . 8 |- (xFy) = (yFx)
35		ecopopr.ass	. . . . . . . 8 |- ((xFy)Fz) = (xF(yFz))
36		visset 1350	. . . . . . . 8 |- r e. V
37	31, 32, 33, 34, 35, 36	caopr411 3079	. . . . . . 7 |- ((hFt)F(fFr)) = ((fFt)F(hFr))
38		visset 1350	. . . . . . . . 9 |- g e. V
39		visset 1350	. . . . . . . . 9 |- s e. V
40	38, 32, 31, 34, 35, 39	caopr411 3079	. . . . . . . 8 |- ((gFt)F(hFs)) = ((hFt)F(gFs))
41	38, 32, 31, 34, 35, 39	caopr4 3078	. . . . . . . 8 |- ((gFt)F(hFs)) = ((gFh)F(tFs))
42	40, 41	eqtr3 1121	. . . . . . 7 |- ((hFt)F(gFs)) = ((gFh)F(tFs))
43	30, 37, 42	3eqtr4g 1147	. . . . . 6 |- (((fFt) = (gFh) /\ (hFr) = (tFs)) -> ((hFt)F(fFr)) = ((hFt)F(gFs)))
44	29, 43	syl6bi 187	. . . . 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 3018	. . . . . . . . . . 11 |- (gFs) e. V
46		ecopopr.can	. . . . . . . . . . 11 |- ((x e. S /\ y e. S) -> ((xFy) = (xFz) -> y = z))
47	45, 46	caoprcan 3069	. . . . . . . . . 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 3066	. . . . . . . . . 10 |- ((h e. S /\ t e. S) -> (hFt) e. S)
50	48	caoprcl 3066	. . . . . . . . . 10 |- ((f e. S /\ r e. S) -> (fFr) e. S)
51	47, 49, 50	syl2an 349	. . . . . . . . 9 |- (((h e. S /\ t e. S) /\ (f e. S /\ r e. S)) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
52	51	3impb 610	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ f e. S /\ r e. S) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
53	52	3com12 614	. . . . . . 7 |- ((f e. S /\ (h e. S /\ t e. S) /\ r e. S) -> (((hFt)F(fFr)) = ((h