Metamath Proof Explorer

Theorem ecopover

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 an equivalence relation. (Contributed by NM, 16-Feb-1996) (Revised by Mario Carneiro, 12-Aug-2015) (Proof shortened by AV, 1-May-2021)

Ref Expression
Hypotheses ecopopr.1 
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }
ecopopr.com 
|- ( x .+ y ) = ( y .+ x )
ecopopr.cl 
|- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )
ecopopr.ass 
|- ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) )
ecopopr.can 
|- ( ( x e. S /\ y e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )
Assertion ecopover 
|- .~ Er ( S X. S )

Proof

Step Hyp Ref Expression
1 ecopopr.1 
 |-  .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }
2 ecopopr.com 
 |-  ( x .+ y ) = ( y .+ x )
3 ecopopr.cl 
 |-  ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )
4 ecopopr.ass 
 |-  ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) )
5 ecopopr.can 
 |-  ( ( x e. S /\ y e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )
6 1 relopabiv 
 |-  Rel .~
7 1 2 ecopovsym 
 |-  ( f .~ g -> g .~ f )
8 1 2 3 4 5 ecopovtrn 
 |-  ( ( f .~ g /\ g .~ h ) -> f .~ h )
9 vex 
 |-  g e. _V
10 vex 
 |-  h e. _V
11 9 10 2 caovcom 
 |-  ( g .+ h ) = ( h .+ g )
12 1 ecopoveq 
 |-  ( ( ( g e. S /\ h e. S ) /\ ( g e. S /\ h e. S ) ) -> ( <. g , h >. .~ <. g , h >. <-> ( g .+ h ) = ( h .+ g ) ) )
13 11 12 mpbiri 
 |-  ( ( ( g e. S /\ h e. S ) /\ ( g e. S /\ h e. S ) ) -> <. g , h >. .~ <. g , h >. )
14 13 anidms 
 |-  ( ( g e. S /\ h e. S ) -> <. g , h >. .~ <. g , h >. )
15 14 rgen2 
 |-  A. g e. S A. h e. S <. g , h >. .~ <. g , h >.
16 breq12 
 |-  ( ( f = <. g , h >. /\ f = <. g , h >. ) -> ( f .~ f <-> <. g , h >. .~ <. g , h >. ) )
17 16 anidms 
 |-  ( f = <. g , h >. -> ( f .~ f <-> <. g , h >. .~ <. g , h >. ) )
18 17 ralxp 
 |-  ( A. f e. ( S X. S ) f .~ f <-> A. g e. S A. h e. S <. g , h >. .~ <. g , h >. )
19 15 18 mpbir 
 |-  A. f e. ( S X. S ) f .~ f
20 19 rspec 
 |-  ( f e. ( S X. S ) -> f .~ f )
21 opabssxp 
 |-  { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) } C_ ( ( S X. S ) X. ( S X. S ) )
22 1 21 eqsstri 
 |-  .~ C_ ( ( S X. S ) X. ( S X. S ) )
23 22 ssbri 
 |-  ( f .~ f -> f ( ( S X. S ) X. ( S X. S ) ) f )
24 brxp 
 |-  ( f ( ( S X. S ) X. ( S X. S ) ) f <-> ( f e. ( S X. S ) /\ f e. ( S X. S ) ) )
25 24 simplbi 
 |-  ( f ( ( S X. S ) X. ( S X. S ) ) f -> f e. ( S X. S ) )
26 23 25 syl 
 |-  ( f .~ f -> f e. ( S X. S ) )
27 20 26 impbii 
 |-  ( f e. ( S X. S ) <-> f .~ f )
28 6 7 8 27 iseri 
 |-  .~ Er ( S X. S )