This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ecopover

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)

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

Proof

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