Theorem ecopover 8568

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.) (Proof shortened by AV, 1-May-2021.)

Hypotheses

Ref	Expression
ecopopr.1	⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}
ecopopr.com	⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
ecopopr.cl	⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
ecopopr.ass	⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
ecopopr.can	⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))

Assertion

Ref	Expression
ecopover	⊢ ∼ Er (𝑆 × 𝑆)

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢, +   𝑥,𝑆,𝑦,𝑧,𝑤,𝑣,𝑢

Allowed substitution hints:   ∼ (𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)

Proof of Theorem ecopover

Dummy variables 𝑓 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ecopopr.1	. . 3 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}
2	1	relopabiv 5719	. 2 ⊢ Rel ∼
3		ecopopr.com	. . 3 ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
4	1, 3	ecopovsym 8566	. 2 ⊢ (𝑓 ∼ 𝑔 → 𝑔 ∼ 𝑓)
5		ecopopr.cl	. . 3 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
6		ecopopr.ass	. . 3 ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
7		ecopopr.can	. . 3 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))
8	1, 3, 5, 6, 7	ecopovtrn 8567	. 2 ⊢ ((𝑓 ∼ 𝑔 ∧ 𝑔 ∼ ℎ) → 𝑓 ∼ ℎ)
9		vex 3426	. . . . . . . . 9 ⊢ 𝑔 ∈ V
10		vex 3426	. . . . . . . . 9 ⊢ ℎ ∈ V
11	9, 10, 3	caovcom 7447	. . . . . . . 8 ⊢ (𝑔 + ℎ) = (ℎ + 𝑔)
12	1	ecopoveq 8565	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → (⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩ ↔ (𝑔 + ℎ) = (ℎ + 𝑔)))
13	11, 12	mpbiri 257	. . . . . . 7 ⊢ (((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩)
14	13	anidms 566	. . . . . 6 ⊢ ((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) → ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩)
15	14	rgen2 3126	. . . . 5 ⊢ ∀𝑔 ∈ 𝑆 ∀ℎ ∈ 𝑆 ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩
16		breq12 5075	. . . . . . 7 ⊢ ((𝑓 = ⟨𝑔, ℎ⟩ ∧ 𝑓 = ⟨𝑔, ℎ⟩) → (𝑓 ∼ 𝑓 ↔ ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩))
17	16	anidms 566	. . . . . 6 ⊢ (𝑓 = ⟨𝑔, ℎ⟩ → (𝑓 ∼ 𝑓 ↔ ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩))
18	17	ralxp 5739	. . . . 5 ⊢ (∀𝑓 ∈ (𝑆 × 𝑆)𝑓 ∼ 𝑓 ↔ ∀𝑔 ∈ 𝑆 ∀ℎ ∈ 𝑆 ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩)
19	15, 18	mpbir 230	. . . 4 ⊢ ∀𝑓 ∈ (𝑆 × 𝑆)𝑓 ∼ 𝑓
20	19	rspec 3131	. . 3 ⊢ (𝑓 ∈ (𝑆 × 𝑆) → 𝑓 ∼ 𝑓)
21		opabssxp 5669	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
22	1, 21	eqsstri 3951	. . . . 5 ⊢ ∼ ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
23	22	ssbri 5115	. . . 4 ⊢ (𝑓 ∼ 𝑓 → 𝑓((𝑆 × 𝑆) × (𝑆 × 𝑆))𝑓)
24		brxp 5627	. . . . 5 ⊢ (𝑓((𝑆 × 𝑆) × (𝑆 × 𝑆))𝑓 ↔ (𝑓 ∈ (𝑆 × 𝑆) ∧ 𝑓 ∈ (𝑆 × 𝑆)))
25	24	simplbi 497	. . . 4 ⊢ (𝑓((𝑆 × 𝑆) × (𝑆 × 𝑆))𝑓 → 𝑓 ∈ (𝑆 × 𝑆))
26	23, 25	syl 17	. . 3 ⊢ (𝑓 ∼ 𝑓 → 𝑓 ∈ (𝑆 × 𝑆))
27	20, 26	impbii 208	. 2 ⊢ (𝑓 ∈ (𝑆 × 𝑆) ↔ 𝑓 ∼ 𝑓)
28	2, 4, 8, 27	iseri 8483	1 ⊢ ∼ Er (𝑆 × 𝑆)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∀wral 3063  ⟨cop 4564   class class class wbr 5070  {copab 5132   × cxp 5578  (class class class)co 7255   Er wer 8453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fv 6426  df-ov 7258  df-er 8456

This theorem is referenced by:  enqer  10608  enrer  10750