# Metamath Proof Explorer

## Theorem ecopovtrn

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 .~ , specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses ecopopr.1
ecopopr.com
ecopopr.cl
ecopopr.ass
ecopopr.can
Assertion ecopovtrn

### Proof

Step Hyp Ref Expression
1 ecopopr.1
2 ecopopr.com
3 ecopopr.cl
4 ecopopr.ass
5 ecopopr.can
6 opabssxp
7 1 6 eqsstri
8 7 brel
9 8 simpld
10 7 brel
11 9 10 anim12i
12 3anass ${⊢}\left({A}\in \left({S}×{S}\right)\wedge {B}\in \left({S}×{S}\right)\wedge {C}\in \left({S}×{S}\right)\right)↔\left({A}\in \left({S}×{S}\right)\wedge \left({B}\in \left({S}×{S}\right)\wedge {C}\in \left({S}×{S}\right)\right)\right)$
13 11 12 sylibr
14 eqid ${⊢}{S}×{S}={S}×{S}$
15 breq1
16 15 anbi1d
17 breq1
18 16 17 imbi12d
19 breq2
20 breq1
21 19 20 anbi12d
22 21 imbi1d
23 breq2
24 23 anbi2d
25 breq2
26 24 25 imbi12d
27 1 ecopoveq
29 1 ecopoveq
31 28 30 anbi12d
32 oveq12
33 vex ${⊢}{h}\in \mathrm{V}$
34 vex ${⊢}{t}\in \mathrm{V}$
35 vex ${⊢}{f}\in \mathrm{V}$
36 vex ${⊢}{r}\in \mathrm{V}$
37 33 34 35 2 4 36 caov411
38 vex ${⊢}{g}\in \mathrm{V}$
39 vex ${⊢}{s}\in \mathrm{V}$
40 38 34 33 2 4 39 caov411
41 38 34 33 2 4 39 caov4
42 40 41 eqtr3i
43 32 37 42 3eqtr4g
44 31 43 syl6bi
45 3 caovcl
46 3 caovcl
47 ovex
48 47 5 caovcan
49 45 46 48 syl2an
50 49 3impb
51 50 3com12
54 44 53 syld
55 1 ecopoveq