Theorem ecopover 8016

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	relopabi 5399	. 2 ⊢ Rel ∼
3		ecopopr.com	. . 3 ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
4	1, 3	ecopovsym 8014	. 2 ⊢ (𝑓 ∼ 𝑔 → 𝑔 ∼ 𝑓)
5		ecopopr.cl	. . 3 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
6		ecopopr.ass	. . 3 ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
7		ecopopr.can	. . 3 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))
8	1, 3, 5, 6, 7	ecopovtrn 8015	. 2 ⊢ ((𝑓 ∼ 𝑔 ∧ 𝑔 ∼ ℎ) → 𝑓 ∼ ℎ)
9		vex 3341	. . . . . . . . 9 ⊢ 𝑔 ∈ V
10		vex 3341	. . . . . . . . 9 ⊢ ℎ ∈ V
11	9, 10, 3	caovcom 6994	. . . . . . . 8 ⊢ (𝑔 + ℎ) = (ℎ + 𝑔)
12	1	ecopoveq 8013	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → (⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩ ↔ (𝑔 + ℎ) = (ℎ + 𝑔)))
13	11, 12	mpbiri 248	. . . . . . 7 ⊢ (((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩)
14	13	anidms 680	. . . . . 6 ⊢ ((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) → ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩)
15	14	rgen2a 3113	. . . . 5 ⊢ ∀𝑔 ∈ 𝑆 ∀ℎ ∈ 𝑆 ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩
16		breq12 4807	. . . . . . 7 ⊢ ((𝑓 = ⟨𝑔, ℎ⟩ ∧ 𝑓 = ⟨𝑔, ℎ⟩) → (𝑓 ∼ 𝑓 ↔ ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩))
17	16	anidms 680	. . . . . 6 ⊢ (𝑓 = ⟨𝑔, ℎ⟩ → (𝑓 ∼ 𝑓 ↔ ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩))
18	17	ralxp 5417	. . . . 5 ⊢ (∀𝑓 ∈ (𝑆 × 𝑆)𝑓 ∼ 𝑓 ↔ ∀𝑔 ∈ 𝑆 ∀ℎ ∈ 𝑆 ⟨𝑔, ℎ⟩ ∼ ⟨𝑔, ℎ⟩)
19	15, 18	mpbir 221	. . . 4 ⊢ ∀𝑓 ∈ (𝑆 × 𝑆)𝑓 ∼ 𝑓
20	19	rspec 3067	. . 3 ⊢ (𝑓 ∈ (𝑆 × 𝑆) → 𝑓 ∼ 𝑓)
21		opabssxp 5348	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
22	1, 21	eqsstri 3774	. . . . 5 ⊢ ∼ ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
23	22	ssbri 4847	. . . 4 ⊢ (𝑓 ∼ 𝑓 → 𝑓((𝑆 × 𝑆) × (𝑆 × 𝑆))𝑓)
24		brxp 5302	. . . . 5 ⊢ (𝑓((𝑆 × 𝑆) × (𝑆 × 𝑆))𝑓 ↔ (𝑓 ∈ (𝑆 × 𝑆) ∧ 𝑓 ∈ (𝑆 × 𝑆)))
25	24	simplbi 478	. . . 4 ⊢ (𝑓((𝑆 × 𝑆) × (𝑆 × 𝑆))𝑓 → 𝑓 ∈ (𝑆 × 𝑆))
26	23, 25	syl 17	. . 3 ⊢ (𝑓 ∼ 𝑓 → 𝑓 ∈ (𝑆 × 𝑆))
27	20, 26	impbii 199	. 2 ⊢ (𝑓 ∈ (𝑆 × 𝑆) ↔ 𝑓 ∼ 𝑓)
28	2, 4, 8, 27	iseri 7936	1 ⊢ ∼ Er (𝑆 × 𝑆)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1630  ∃wex 1851   ∈ wcel 2137  ∀wral 3048  ⟨cop 4325   class class class wbr 4802  {copab 4862   × cxp 5262  (class class class)co 6811   Er wer 7906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pr 5053

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-iun 4672  df-br 4803  df-opab 4863  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-iota 6010  df-fv 6055  df-ov 6814  df-er 7909

This theorem is referenced by:  enqer  9933  enrer  10076