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	⊢ ( 𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴 )