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

Metamath Proof Explorer

Theorem ecopovsym

Description: Assuming the operation F is commutative, show that the relation .~ , specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 ecopopr.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) }
2 ecopopr.com ⊢ ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 )
3 opabssxp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑆 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑆 × 𝑆 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑦 = ⟨ 𝑣 , 𝑢 ⟩ ) ∧ ( 𝑧 + 𝑢 ) = ( 𝑤 + 𝑣 ) ) ) } ⊆ ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) )
4 1 3 eqsstri ⊢ ∼ ⊆ ( ( 𝑆 × 𝑆 ) × ( 𝑆 × 𝑆 ) )
5 4 brel ⊢ ( 𝐴 ∼ 𝐵 → ( 𝐴 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐵 ∈ ( 𝑆 × 𝑆 ) ) )
6 eqid ⊢ ( 𝑆 × 𝑆 ) = ( 𝑆 × 𝑆 )
7 breq1 ⊢ ( ⟨ 𝑓 , 𝑔 ⟩ = 𝐴 → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ↔ 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ) )
8 breq2 ⊢ ( ⟨ 𝑓 , 𝑔 ⟩ = 𝐴 → ( ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑓 , 𝑔 ⟩ ↔ ⟨ ℎ , 𝑡 ⟩ ∼ 𝐴 ) )
9 7 8 bibi12d ⊢ ( ⟨ 𝑓 , 𝑔 ⟩ = 𝐴 → ( ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ↔ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑓 , 𝑔 ⟩ ) ↔ ( 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ↔ ⟨ ℎ , 𝑡 ⟩ ∼ 𝐴 ) ) )
10 breq2 ⊢ ( ⟨ ℎ , 𝑡 ⟩ = 𝐵 → ( 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ↔ 𝐴 ∼ 𝐵 ) )
11 breq1 ⊢ ( ⟨ ℎ , 𝑡 ⟩ = 𝐵 → ( ⟨ ℎ , 𝑡 ⟩ ∼ 𝐴 ↔ 𝐵 ∼ 𝐴 ) )
12 10 11 bibi12d ⊢ ( ⟨ ℎ , 𝑡 ⟩ = 𝐵 → ( ( 𝐴 ∼ ⟨ ℎ , 𝑡 ⟩ ↔ ⟨ ℎ , 𝑡 ⟩ ∼ 𝐴 ) ↔ ( 𝐴 ∼ 𝐵 ↔ 𝐵 ∼ 𝐴 ) ) )
13 1 ecopoveq ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ) → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ↔ ( 𝑓 + 𝑡 ) = ( 𝑔 + ℎ ) ) )
14 vex ⊢ 𝑓 ∈ V
15 vex ⊢ 𝑡 ∈ V
16 14 15 2 caovcom ⊢ ( 𝑓 + 𝑡 ) = ( 𝑡 + 𝑓 )
17 vex ⊢ 𝑔 ∈ V
18 vex ⊢ ℎ ∈ V
19 17 18 2 caovcom ⊢ ( 𝑔 + ℎ ) = ( ℎ + 𝑔 )
20 16 19 eqeq12i ⊢ ( ( 𝑓 + 𝑡 ) = ( 𝑔 + ℎ ) ↔ ( 𝑡 + 𝑓 ) = ( ℎ + 𝑔 ) )
21 eqcom ⊢ ( ( 𝑡 + 𝑓 ) = ( ℎ + 𝑔 ) ↔ ( ℎ + 𝑔 ) = ( 𝑡 + 𝑓 ) )
22 20 21 bitri ⊢ ( ( 𝑓 + 𝑡 ) = ( 𝑔 + ℎ ) ↔ ( ℎ + 𝑔 ) = ( 𝑡 + 𝑓 ) )
23 13 22 bitrdi ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ) → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ↔ ( ℎ + 𝑔 ) = ( 𝑡 + 𝑓 ) ) )
24 1 ecopoveq ⊢ ( ( ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ) → ( ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑓 , 𝑔 ⟩ ↔ ( ℎ + 𝑔 ) = ( 𝑡 + 𝑓 ) ) )
25 24 ancoms ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ) → ( ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑓 , 𝑔 ⟩ ↔ ( ℎ + 𝑔 ) = ( 𝑡 + 𝑓 ) ) )
26 23 25 bitr4d ⊢ ( ( ( 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆 ) ∧ ( ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆 ) ) → ( ⟨ 𝑓 , 𝑔 ⟩ ∼ ⟨ ℎ , 𝑡 ⟩ ↔ ⟨ ℎ , 𝑡 ⟩ ∼ ⟨ 𝑓 , 𝑔 ⟩ ) )
27 6 9 12 26 2optocl ⊢ ( ( 𝐴 ∈ ( 𝑆 × 𝑆 ) ∧ 𝐵 ∈ ( 𝑆 × 𝑆 ) ) → ( 𝐴 ∼ 𝐵 ↔ 𝐵 ∼ 𝐴 ) )
28 5 27 syl ⊢ ( 𝐴 ∼ 𝐵 → ( 𝐴 ∼ 𝐵 ↔ 𝐵 ∼ 𝐴 ) )
29 28 ibi ⊢ ( 𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴 )