Theorem ecopover 6140

Description: Assuming that operation 𝐹 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.)

Hypotheses

Ref	Expression
ecopopr.1	⊢ ∼ = {⟨x, y⟩ ∣ ((x ∈ (𝑆 × 𝑆) ∧ y ∈ (𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z + u) = (w + v)))}
ecopopr.com	⊢ (x + y) = (y + x)
ecopopr.cl	⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → (x + y) ∈ 𝑆)
ecopopr.ass	⊢ ((x + y) + z) = (x + (y + z))
ecopopr.can	⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → ((x + y) = (x + z) → y = z))

Assertion

Ref	Expression
ecopover	⊢ ∼ Er (𝑆 × 𝑆)

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

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

Proof of Theorem ecopover

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

Step	Hyp	Ref	Expression
1		ecopopr.1	. . . . 5 ⊢ ∼ = {⟨x, y⟩ ∣ ((x ∈ (𝑆 × 𝑆) ∧ y ∈ (𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z + u) = (w + v)))}
2	1	relopabi 4406	. . . 4 ⊢ Rel ∼
3	2	a1i 9	. . 3 ⊢ ( ⊤ → Rel ∼ )
4		ecopopr.com	. . . . 5 ⊢ (x + y) = (y + x)
5	1, 4	ecopovsym 6138	. . . 4 ⊢ (f ∼ g → g ∼ f)
6	5	adantl 262	. . 3 ⊢ (( ⊤ ∧ f ∼ g) → g ∼ f)
7		ecopopr.cl	. . . . 5 ⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → (x + y) ∈ 𝑆)
8		ecopopr.ass	. . . . 5 ⊢ ((x + y) + z) = (x + (y + z))
9		ecopopr.can	. . . . 5 ⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → ((x + y) = (x + z) → y = z))
10	1, 4, 7, 8, 9	ecopovtrn 6139	. . . 4 ⊢ ((f ∼ g ∧ g ∼ ℎ) → f ∼ ℎ)
11	10	adantl 262	. . 3 ⊢ (( ⊤ ∧ (f ∼ g ∧ g ∼ ℎ)) → f ∼ ℎ)
12		vex 2554	. . . . . . . . . . 11 ⊢ g ∈ V
13		vex 2554	. . . . . . . . . . 11 ⊢ ℎ ∈ V
14	12, 13, 4	caovcom 5600	. . . . . . . . . 10 ⊢ (g + ℎ) = (ℎ + g)
15	1	ecopoveq 6137	. . . . . . . . . 10 ⊢ (((g ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (g ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → (⟨g, ℎ⟩ ∼ ⟨g, ℎ⟩ ↔ (g + ℎ) = (ℎ + g)))
16	14, 15	mpbiri 157	. . . . . . . . 9 ⊢ (((g ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (g ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → ⟨g, ℎ⟩ ∼ ⟨g, ℎ⟩)
17	16	anidms 377	. . . . . . . 8 ⊢ ((g ∈ 𝑆 ∧ ℎ ∈ 𝑆) → ⟨g, ℎ⟩ ∼ ⟨g, ℎ⟩)
18	17	rgen2a 2369	. . . . . . 7 ⊢ ∀g ∈ 𝑆 ∀ℎ ∈ 𝑆 ⟨g, ℎ⟩ ∼ ⟨g, ℎ⟩
19		breq12 3760	. . . . . . . . 9 ⊢ ((f = ⟨g, ℎ⟩ ∧ f = ⟨g, ℎ⟩) → (f ∼ f ↔ ⟨g, ℎ⟩ ∼ ⟨g, ℎ⟩))
20	19	anidms 377	. . . . . . . 8 ⊢ (f = ⟨g, ℎ⟩ → (f ∼ f ↔ ⟨g, ℎ⟩ ∼ ⟨g, ℎ⟩))
21	20	ralxp 4422	. . . . . . 7 ⊢ (∀f ∈ (𝑆 × 𝑆)f ∼ f ↔ ∀g ∈ 𝑆 ∀ℎ ∈ 𝑆 ⟨g, ℎ⟩ ∼ ⟨g, ℎ⟩)
22	18, 21	mpbir 134	. . . . . 6 ⊢ ∀f ∈ (𝑆 × 𝑆)f ∼ f
23	22	rspec 2367	. . . . 5 ⊢ (f ∈ (𝑆 × 𝑆) → f ∼ f)
24	23	a1i 9	. . . 4 ⊢ ( ⊤ → (f ∈ (𝑆 × 𝑆) → f ∼ f))
25		opabssxp 4357	. . . . . . 7 ⊢ {⟨x, y⟩ ∣ ((x ∈ (𝑆 × 𝑆) ∧ y ∈ (𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z + u) = (w + v)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
26	1, 25	eqsstri 2969	. . . . . 6 ⊢ ∼ ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
27	26	ssbri 3797	. . . . 5 ⊢ (f ∼ f → f((𝑆 × 𝑆) × (𝑆 × 𝑆))f)
28		brxp 4318	. . . . . 6 ⊢ (f((𝑆 × 𝑆) × (𝑆 × 𝑆))f ↔ (f ∈ (𝑆 × 𝑆) ∧ f ∈ (𝑆 × 𝑆)))
29	28	simplbi 259	. . . . 5 ⊢ (f((𝑆 × 𝑆) × (𝑆 × 𝑆))f → f ∈ (𝑆 × 𝑆))
30	27, 29	syl 14	. . . 4 ⊢ (f ∼ f → f ∈ (𝑆 × 𝑆))
31	24, 30	impbid1 130	. . 3 ⊢ ( ⊤ → (f ∈ (𝑆 × 𝑆) ↔ f ∼ f))
32	3, 6, 11, 31	iserd 6068	. 2 ⊢ ( ⊤ → ∼ Er (𝑆 × 𝑆))
33	32	trud 1251	1 ⊢ ∼ Er (𝑆 × 𝑆)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242   ⊤ wtru 1243  ∃wex 1378   ∈ wcel 1390  ∀wral 2300  ⟨cop 3370   class class class wbr 3755  {copab 3808   × 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-bnd 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: (None)