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 ( 𝑆 × 𝑆 )