Theorem ecopoverg 6143

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 Jim Kingdon, 1-Sep-2019.)

Hypotheses

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

Assertion

Ref	Expression
ecopoverg	|- .~ 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 ecopoverg

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

Step	Hyp	Ref	Expression
1		ecopopr.1	. . . . 5 |- .~ = { <.x , y >. | ((x e. ( S X. S) /\ y e. ( S X. S)) /\ E.zE.wE.vE.u((x = <.z , w >. /\ y = <.v , u >.) /\ (z .+ u) = (w .+ v))) }
2	1	relopabi 4406	. . . 4 |- Rel .~
3	2	a1i 9	. . 3 |- ( T. -> Rel .~ )
4		ecopoprg.com	. . . . 5 |- ((x e. S /\ y e. S) -> (x .+ y) = (y .+ x))
5	1, 4	ecopovsymg 6141	. . . 4 |- (f .~ g -> g .~ f)
6	5	adantl 262	. . 3 |- (( T. /\ f .~ g) -> g .~ f)
7		ecopoprg.cl	. . . . 5 |- ((x e. S /\ y e. S) -> (x .+ y) e. S)
8		ecopoprg.ass	. . . . 5 |- ((x e. S /\ y e. S /\ z e. S) -> ((x .+ y) .+ z) = (x .+ (y .+ z)))
9		ecopoprg.can	. . . . 5 |- ((x e. S /\ y e. S /\ z e. S) -> ((x .+ y) = (x .+ z) -> y = z))
10	1, 4, 7, 8, 9	ecopovtrng 6142	. . . 4 |- ((f .~ g /\ g .~ h) -> f .~ h)
11	10	adantl 262	. . 3 |- (( T. /\ (f .~ g /\ g .~ h)) -> f .~ h)
12	4	adantl 262	. . . . . . . . . . 11 |- ((((g e. S /\ h e. S) /\ (g e. S /\ h e. S)) /\ (x e. S /\ y e. S)) -> (x .+ y) = (y .+ x))
13		simpll 481	. . . . . . . . . . 11 |- (((g e. S /\ h e. S) /\ (g e. S /\ h e. S)) -> g e. S)
14		simplr 482	. . . . . . . . . . 11 |- (((g e. S /\ h e. S) /\ (g e. S /\ h e. S)) -> h e. S)
15	12, 13, 14	caovcomd 5599	. . . . . . . . . 10 |- (((g e. S /\ h e. S) /\ (g e. S /\ h e. S)) -> (g .+ h) = ( h .+ g))
16	1	ecopoveq 6137	. . . . . . . . . 10 |- (((g e. S /\ h e. S) /\ (g e. S /\ h e. S)) -> ( <.g , h >. .~ <.g , h >. <-> (g .+ h) = ( h .+ g)))
17	15, 16	mpbird 156	. . . . . . . . 9 |- (((g e. S /\ h e. S) /\ (g e. S /\ h e. S)) -> <.g , h >. .~ <.g , h >.)
18	17	anidms 377	. . . . . . . 8 |- ((g e. S /\ h e. S) -> <.g , h >. .~ <.g , h >.)
19	18	rgen2a 2369	. . . . . . 7 |- A.g e. S A. h e. S <.g , h >. .~ <.g , h >.
20		breq12 3760	. . . . . . . . 9 |- ((f = <.g , h >. /\ f = <.g , h >.) -> (f .~ f <-> <.g , h >. .~ <.g , h >.))
21	20	anidms 377	. . . . . . . 8 |- (f = <.g , h >. -> (f .~ f <-> <.g , h >. .~ <.g , h >.))
22	21	ralxp 4422	. . . . . . 7 |- (A.f e. ( S X. S)f .~ f <-> A.g e. S A. h e. S <.g , h >. .~ <.g , h >.)
23	19, 22	mpbir 134	. . . . . 6 |- A.f e. ( S X. S)f .~ f
24	23	rspec 2367	. . . . 5 |- (f e. ( S X. S) -> f .~ f)
25	24	a1i 9	. . . 4 |- ( T. -> (f e. ( S X. S) -> f .~ f))
26		opabssxp 4357	. . . . . . 7 |- { <.x , y >. | ((x e. ( S X. S) /\ y e. ( S X. S)) /\ E.zE.wE.vE.u((x = <.z , w >. /\ y = <.v , u >.) /\ (z .+ u) = (w .+ v))) } C_ (( S X. S) X. ( S X. S))
27	1, 26	eqsstri 2969	. . . . . 6 |- .~ C_ (( S X. S) X. ( S X. S))
28	27	ssbri 3797	. . . . 5 |- (f .~ f -> f(( S X. S) X. ( S X. S))f)
29		brxp 4318	. . . . . 6 |- (f(( S X. S) X. ( S X. S))f <-> (f e. ( S X. S) /\ f e. ( S X. S)))
30	29	simplbi 259	. . . . 5 |- (f(( S X. S) X. ( S X. S))f -> f e. ( S X. S))
31	28, 30	syl 14	. . . 4 |- (f .~ f -> f e. ( S X. S))
32	25, 31	impbid1 130	. . 3 |- ( T. -> (f e. ( S X. S) <-> f .~ f))
33	3, 6, 11, 32	iserd 6068	. 2 |- ( T. -> .~ Er ( S X. S))
34	33	trud 1251	1 |- .~ Er ( S X. S)

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   /\ w3a 884   = wceq 1242   T. wtru 1243  E.wex 1378   e. wcel 1390  A.wral 2300   <.cop 3370   class class class wbr 3755   {copab 3808   X. cxp 4286   Rel wrel 4293  (class class class)co 5455   Er wer 6039

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-iun 3650  df-br 3756  df-opab 3810  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-iota 4810  df-fv 4853  df-ov 5458  df-er 6042

This theorem is referenced by:  enqer  6342  enrer  6663