Theorem ecopover 7851

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
ecopover	|- .~ Er ( S X. S )

Distinct variable groups:   x, y, z, w, v, u, .+   x, S, y, z, w, v, u

Allowed substitution hints:   .~ ( x, y, z, w, v, u)

Proof of Theorem ecopover

Dummy variables f g h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ecopopr.1	. . 3 |- .~ = { <. 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	1	relopabi 5245	. 2 |- Rel .~
3		ecopopr.com	. . 3 |- ( x .+ y ) = ( y .+ x )
4	1, 3	ecopovsym 7849	. 2 |- ( f .~ g -> g .~ f )
5		ecopopr.cl	. . 3 |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )
6		ecopopr.ass	. . 3 |- ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) )
7		ecopopr.can	. . 3 |- ( ( x e. S /\ y e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )
8	1, 3, 5, 6, 7	ecopovtrn 7850	. 2 |- ( ( f .~ g /\ g .~ h ) -> f .~ h )
9		vex 3203	. . . . . . . . 9 |- g e. _V
10		vex 3203	. . . . . . . . 9 |- h e. _V
11	9, 10, 3	caovcom 6831	. . . . . . . 8 |- ( g .+ h ) = ( h .+ g )
12	1	ecopoveq 7848	. . . . . . . 8 |- ( ( ( g e. S /\ h e. S ) /\ ( g e. S /\ h e. S ) ) -> ( <. g , h >. .~ <. g , h >. <-> ( g .+ h ) = ( h .+ g ) ) )
13	11, 12	mpbiri 248	. . . . . . 7 |- ( ( ( g e. S /\ h e. S ) /\ ( g e. S /\ h e. S ) ) -> <. g , h >. .~ <. g , h >. )
14	13	anidms 677	. . . . . 6 |- ( ( g e. S /\ h e. S ) -> <. g , h >. .~ <. g , h >. )
15	14	rgen2a 2977	. . . . 5 |- A. g e. S A. h e. S <. g , h >. .~ <. g , h >.
16		breq12 4658	. . . . . . 7 |- ( ( f = <. g , h >. /\ f = <. g , h >. ) -> ( f .~ f <-> <. g , h >. .~ <. g , h >. ) )
17	16	anidms 677	. . . . . 6 |- ( f = <. g , h >. -> ( f .~ f <-> <. g , h >. .~ <. g , h >. ) )
18	17	ralxp 5263	. . . . 5 |- ( A. f e. ( S X. S ) f .~ f <-> A. g e. S A. h e. S <. g , h >. .~ <. g , h >. )
19	15, 18	mpbir 221	. . . 4 |- A. f e. ( S X. S ) f .~ f
20	19	rspec 2931	. . 3 |- ( f e. ( S X. S ) -> f .~ f )
21		opabssxp 5193	. . . . . 6 |- { <. 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 3635	. . . . 5 |- .~ C_ ( ( S X. S ) X. ( S X. S ) )
23	22	ssbri 4697	. . . 4 |- ( f .~ f -> f ( ( S X. S ) X. ( S X. S ) ) f )
24		brxp 5147	. . . . 5 |- ( f ( ( S X. S ) X. ( S X. S ) ) f <-> ( f e. ( S X. S ) /\ f e. ( S X. S ) ) )
25	24	simplbi 476	. . . 4 |- ( f ( ( S X. S ) X. ( S X. S ) ) f -> f e. ( S X. S ) )
26	23, 25	syl 17	. . 3 |- ( f .~ f -> f e. ( S X. S ) )
27	20, 26	impbii 199	. 2 |- ( f e. ( S X. S ) <-> f .~ f )
28	2, 4, 8, 27	iseri 7769	1 |- .~ Er ( S X. S )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   <.cop 4183   class class class wbr 4653   {copab 4712   X. cxp 5112  (class class class)co 6650   Er wer 7739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fv 5896  df-ov 6653  df-er 7742

This theorem is referenced by:  enqer  9743  enrer  9886