Theorem ecopoprtrn 5531

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 4193	. . . . . . 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)))} C_ ((S X. S) X. (S X. S))
4	2, 3	eqsstri 2874	. . . . . 6 |- R C_ ((S X. S) X. (S X. S))
5	1, 4	brel 4181	. . . . 5 |- (ARB -> (A e. (S X. S) /\ B e. (S X. S)))
6	5	simpld 440	. . . 4 |- (ARB -> A e. (S X. S))
7		ecopopr.4	. . . . 5 |- C e. _V
8	7, 4	brel 4181	. . . 4 |- (BRC -> (B e. (S X. S) /\ C e. (S X. S)))
9	6, 8	anim12i 536	. . 3 |- ((ARB /\ BRC) -> (A e. (S X. S) /\ (B e. (S X. S) /\ C e. (S X. S))))
10		3anass 1106	. . 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 243	. 2 |- ((ARB /\ BRC) -> (A e. (S X. S) /\ B e. (S X. S) /\ C e. (S X. S)))
12		eqid 2141	. . 3 |- (S X. S) = (S X. S)
13		breq1 3510	. . . . 5 |- (<.f, g>. = A -> (<.f, g>.R<.h, t>. <-> AR<.h, t>.))
14	13	anbi1d 752	. . . 4 |- (<.f, g>. = A -> ((<.f, g>.R<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (AR<.h, t>. /\ <.h, t>.R<.s, r>.)))
15		breq1 3510	. . . 4 |- (<.f, g>. = A -> (<.f, g>.R<.s, r>. <-> AR<.s, r>.))
16	14, 15	imbi12d 761	. . 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 3511	. . . . 5 |- (<.h, t>. = B -> (AR<.h, t>. <-> ARB))
18		breq1 3510	. . . . 5 |- (<.h, t>. = B -> (<.h, t>.R<.s, r>. <-> BR<.s, r>.))
19	17, 18	anbi12d 763	. . . 4 |- (<.h, t>. = B -> ((AR<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (ARB /\ BR<.s, r>.)))
20	19	imbi1d 748	. . 3 |- (<.h, t>. = B -> (((AR<.h, t>. /\ <.h, t>.R<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BR<.s, r>.) -> AR<.s, r>.)))
21		breq2 3511	. . . . 5 |- (<.s, r>. = C -> (BR<.s, r>. <-> BRC))
22	21	anbi2d 751	. . . 4 |- (<.s, r>. = C -> ((ARB /\ BR<.s, r>.) <-> (ARB /\ BRC)))
23		breq2 3511	. . . 4 |- (<.s, r>. = C -> (AR<.s, r>. <-> ARC))
24	22, 23	imbi12d 761	. . 3 |- (<.s, r>. = C -> (((ARB /\ BR<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BRC) -> ARC)))
25	2	ecopopreq 5528	. . . . . . . 8 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S)) -> (<.f, g>.R<.h, t>. <-> (fFt) = (gFh)))
26	25	3adant3 1140	. . . . . . 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 5528	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (<.h, t>.R<.s, r>. <-> (hFr) = (tFs)))
28	27	3adant1 1138	. . . . . . 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 763	. . . . . 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 4988	. . . . . . 7 |- (((fFt) = (gFh) /\ (hFr) = (tFs)) -> ((fFt)F(hFr)) = ((gFh)F(tFs)))
31		visset 2541	. . . . . . . 8 |- h e. _V
32		visset 2541	. . . . . . . 8 |- t e. _V
33		visset 2541	. . . . . . . 8 |- f e. _V
34		ecopopr.com	. . . . . . . 8 |- (xFy) = (yFx)
35		ecopopr.ass	. . . . . . . 8 |- ((xFy)Fz) = (xF(yFz))
36		visset 2541	. . . . . . . 8 |- r e. _V
37	31, 32, 33, 34, 35, 36	caopr411 5091	. . . . . . 7 |- ((hFt)F(fFr)) = ((fFt)F(hFr))
38		visset 2541	. . . . . . . . 9 |- g e. _V
39		visset 2541	. . . . . . . . 9 |- s e. _V
40	38, 32, 31, 34, 35, 39	caopr411 5091	. . . . . . . 8 |- ((gFt)F(hFs)) = ((hFt)F(gFs))
41	38, 32, 31, 34, 35, 39	caopr4 5090	. . . . . . . 8 |- ((gFt)F(hFs)) = ((gFh)F(tFs))
42	40, 41	eqtr3i 2163	. . . . . . 7 |- ((hFt)F(gFs)) = ((gFh)F(tFs))
43	30, 37, 42	3eqtr4g 2201	. . . . . 6 |- (((fFt) = (gFh) /\ (hFr) = (tFs)) -> ((hFt)F(fFr)) = ((hFt)F(gFs)))
44	29, 43	syl6bi 263	. . . . 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		ecopopr.cl	. . . . . . . . . . 11 |- ((x e. S /\ y e. S) -> (xFy) e. S)
46	45	caoprcl 5078	. . . . . . . . . 10 |- ((h e. S /\ t e. S) -> (hFt) e. S)
47	45	caoprcl 5078	. . . . . . . . . 10 |- ((f e. S /\ r e. S) -> (fFr) e. S)
48		oprex 5003	. . . . . . . . . . 11 |- (gFs) e. _V
49		ecopopr.can	. . . . . . . . . . 11 |- ((x e. S /\ y e. S) -> ((xFy) = (xFz) -> y = z))
50	48, 49	caoprcan 5081	. . . . . . . . . 10 |- (((hFt) e. S /\ (fFr) e. S) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
51	46, 47, 50	syl2an 603	. . . . . . . . 9 |- (((h e. S /\ t e. S) /\ (f e. S /\ r e. S)) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
52	51	3impb 1313	. . . . . . . 8 |- (((h e. S /\ t e. S) /\ f e. S /\ r e. S) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
53	52	3com12 1321	. . . . . . 7 |- ((f e. S /\ (h e. S /\ t e. S) /\ r e. S) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
54	53	3adant3l 1343	. . . . . 6 |- ((f e. S /\ (h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
55	54	3adant1r 1340	. . . . 5 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
56	44, 55	syld 33	. . . 4 |- (((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>.) -> (fFr) = (gFs)))
57	2	ecopopreq 5528	. . . . 5 |- (((f e. S /\ g e. S) /\ (s e. S /\ r e. S)) -> (<.f, g>.R<.s, r>. <-> (fFr) = (gFs)))
58	57	3adant2 1139	. . . 4 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (<.f, g>.R<.s, r>. <-> (fFr) = (gFs)))
59	56, 58	sylibrd 247	. . 3 |- (((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>.) -> <.f, g>.R<.s, r>.))
60	12, 16, 20, 24, 59	3optocl 4196	. 2 |- ((A e. (S X. S) /\ B e. (S X. S) /\ C e. (S X. S)) -> ((ARB /\ BRC) -> ARC))
61	11, 60	mpcom 101	1 |- ((ARB /\ BRC) -> ARC)

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  E.wex 1615  _Vcvv 2538  <.cop 3240   class class class wbr 3507  {copab 3565   X. cxp 4117  (class class class)co 4981

This theorem is referenced by:  ecopoprer 5532

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-xp 4133  df-cnv 4135  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fv 4147  df-opr 4983

Copyright terms: Public domain