HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef 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))
42, 3eqsstr 2091 . . . . . 6 |- R (_ ((S X. S) X. (S X. S))
51, 4brel 3223 . . . . 5 |- (ARB -> (A e. (S X. S) /\ B e. (S X. S)))
65pm3.26d 321 . . . 4 |- (ARB -> A e. (S X. S))
7 ecopopr.4 . . . . 5 |- C e. V
87, 4brel 3223 . . . 4 |- (BRC -> (B e. (S X. S) /\ C e. (S X. S)))
96, 8anim12i 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))))
119, 10sylibr 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>.))
1413anbi1d 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>.))
1614, 15imbi12d 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>.))
1917, 18anbi12d 628 . . . 4 |- (<.h, t>. = B -> ((AR<.h, t>. /\ <.h, t>.R<.s, r>.) <-> (ARB /\ BR<.s, r>.)))
2019imbi1d 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))
2221anbi2d 616 . . . 4 |- (<.s, r>. = C -> ((ARB /\ BR<.s, r>.) <-> (ARB /\ BRC)))
23 breq2 2623 . . . 4 |- (<.s, r>. = C -> (AR<.s, r>. <-> ARC))
2422, 23imbi12d 626 . . 3 |- (<.s, r>. = C -> (((ARB /\ BR<.s, r>.) -> AR<.s, r>.) <-> ((ARB /\ BRC) -> ARC)))
252ecopopreq 4308 . . . . . . . 8 |- (((f e. S /\ g e. S) /\ (h e. S /\ t e. S)) -> (<.f, g>.R<.h, t>. <-> (fFt) = (gFh)))
26253adant3 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)))
272ecopopreq 4308 . . . . . . . 8 |- (((h e. S /\ t e. S) /\ (s e. S /\ r e. S)) -> (<.h, t>.R<.s, r>. <-> (hFr) = (tFs)))
28273adant1 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)))
2926, 28anbi12d 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
3731, 32, 33, 34, 35, 36caopr411 4065 . . . . . . 7 |- ((hFt)F(fFr)) = ((fFt)F(hFr))
38 visset 1813 . . . . . . . . 9 |- g e. V
39 visset 1813 . . . . . . . . 9 |- s e. V
4038, 32, 31, 34, 35, 39caopr411 4065 . . . . . . . 8 |- ((gFt)F(hFs)) = ((hFt)F(gFs))
4138, 32, 31, 34, 35, 39caopr4 4064 . . . . . . . 8 |- ((gFt)F(hFs)) = ((gFh)F(tFs))
4240, 41eqtr3 1497 . . . . . . 7 |- ((hFt)F(gFs)) = ((gFh)F(tFs))
4330, 37, 423eqtr4g 1531 . . . . . 6 |- (((fFt) = (gFh) /\ (hFr) = (tFs)) -> ((hFt)F(fFr)) = ((hFt)F(gFs)))
4429, 43syl6bi 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))
4745, 46caoprcan 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)
4948caoprcl 4052 . . . . . . . . . 10 |- ((h e. S /\ t e. S) -> (hFt) e. S)
5048caoprcl 4052 . . . . . . . . . 10 |- ((f e. S /\ r e. S) -> (fFr) e. S)
5147, 49, 50syl2an 454 . . . . . . . . 9 |- (((h e. S /\ t e. S) /\ (f e. S /\ r e. S)) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fFr) = (gFs)))
52513impb 829 . . . . . . . 8 |- (((h e. S /\ t e. S) /\ f e. S /\ r e. S) -> (((hFt)F(fFr)) = ((hFt)F(gFs)) -> (fF