Metamath Proof Explorer

Theorem eceqoveq

Description: Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996) (Proof shortened by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypotheses eceqoveq.5 ⊢ ∼ Er ( 𝑆 × 𝑆 )
eceqoveq.7 ⊢ dom + = ( 𝑆 × 𝑆 )
eceqoveq.8 ⊢ ¬ ∅ ∈ 𝑆
eceqoveq.9 ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
eceqoveq.10 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∼ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )
Assertion eceqoveq ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 eceqoveq.5 ⊢ ∼ Er ( 𝑆 × 𝑆 )
2 eceqoveq.7 ⊢ dom + = ( 𝑆 × 𝑆 )
3 eceqoveq.8 ⊢ ¬ ∅ ∈ 𝑆
4 eceqoveq.9 ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
5 eceqoveq.10 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∼ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )
6 opelxpi ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) )
7 6 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) )
8 1 a1i ⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ∼ Er ( 𝑆 × 𝑆 ) )
9 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ )
10 8 9 ereldm ⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ) )
11 7 10 mpbid ⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) )
12 opelxp2 ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) → 𝐷 ∈ 𝑆 )
13 11 12 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) → 𝐷 ∈ 𝑆 )
14 13 ex ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → 𝐷 ∈ 𝑆 ) )
15 4 caovcl ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐵 + 𝐶 ) ∈ 𝑆 )
16 eleq1 ⊢ ( ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) → ( ( 𝐴 + 𝐷 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐶 ) ∈ 𝑆 ) )
17 15 16 syl5ibr ⊢ ( ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) → ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐴 + 𝐷 ) ∈ 𝑆 ) )
18 2 3 ndmovrcl ⊢ ( ( 𝐴 + 𝐷 ) ∈ 𝑆 → ( 𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) )
19 18 simprd ⊢ ( ( 𝐴 + 𝐷 ) ∈ 𝑆 → 𝐷 ∈ 𝑆 )
20 17 19 syl6com ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) → 𝐷 ∈ 𝑆 ) )
21 20 adantll ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) → ( ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) → 𝐷 ∈ 𝑆 ) )
22 1 a1i ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ∼ Er ( 𝑆 × 𝑆 ) )
23 6 adantr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) )
24 22 23 erth ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∼ ⟨ 𝐶 , 𝐷 ⟩ ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) )
25 24 5 bitr3d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )
26 25 expr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) → ( 𝐷 ∈ 𝑆 → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) ) )
27 14 21 26 pm5.21ndd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )
28 27 an32s ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )
29 eqcom ⊢ ( ∅ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ )
30 erdm ⊢ ( ∼ Er ( 𝑆 × 𝑆 ) → dom ∼ = ( 𝑆 × 𝑆 ) )
31 1 30 ax-mp ⊢ dom ∼ = ( 𝑆 × 𝑆 )
32 31 eleq2i ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ dom ∼ ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) )
33 ecdmn0 ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ dom ∼ ↔ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ≠ ∅ )
34 opelxp ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) )
35 32 33 34 3bitr3i ⊢ ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ≠ ∅ ↔ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) )
36 35 simplbi2 ⊢ ( 𝐶 ∈ 𝑆 → ( 𝐷 ∈ 𝑆 → [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ≠ ∅ ) )
37 36 ad2antlr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( 𝐷 ∈ 𝑆 → [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ≠ ∅ ) )
38 37 necon2bd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ → ¬ 𝐷 ∈ 𝑆 ) )
39 simpr ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → 𝐷 ∈ 𝑆 )
40 39 con3i ⊢ ( ¬ 𝐷 ∈ 𝑆 → ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) )
41 2 ndmov ⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → ( 𝐴 + 𝐷 ) = ∅ )
42 40 41 syl ⊢ ( ¬ 𝐷 ∈ 𝑆 → ( 𝐴 + 𝐷 ) = ∅ )
43 38 42 syl6 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ → ( 𝐴 + 𝐷 ) = ∅ ) )
44 eleq1 ⊢ ( ( 𝐴 + 𝐷 ) = ∅ → ( ( 𝐴 + 𝐷 ) ∈ 𝑆 ↔ ∅ ∈ 𝑆 ) )
45 3 44 mtbiri ⊢ ( ( 𝐴 + 𝐷 ) = ∅ → ¬ ( 𝐴 + 𝐷 ) ∈ 𝑆 )
46 35 simprbi ⊢ ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ≠ ∅ → 𝐷 ∈ 𝑆 )
47 4 caovcl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → ( 𝐴 + 𝐷 ) ∈ 𝑆 )
48 47 ex ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐷 ∈ 𝑆 → ( 𝐴 + 𝐷 ) ∈ 𝑆 ) )
49 48 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( 𝐷 ∈ 𝑆 → ( 𝐴 + 𝐷 ) ∈ 𝑆 ) )
50 46 49 syl5 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ≠ ∅ → ( 𝐴 + 𝐷 ) ∈ 𝑆 ) )
51 50 necon1bd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( ¬ ( 𝐴 + 𝐷 ) ∈ 𝑆 → [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ ) )
52 45 51 syl5 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 + 𝐷 ) = ∅ → [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ ) )
53 43 52 impbid ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ ↔ ( 𝐴 + 𝐷 ) = ∅ ) )
54 29 53 syl5bb ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( ∅ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ∅ ) )
55 31 eleq2i ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ∼ ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) )
56 ecdmn0 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ∼ ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≠ ∅ )
57 opelxp ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
58 55 56 57 3bitr3i ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≠ ∅ ↔ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
59 58 simprbi ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≠ ∅ → 𝐵 ∈ 𝑆 )
60 59 necon1bi ⊢ ( ¬ 𝐵 ∈ 𝑆 → [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = ∅ )
61 60 adantl ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = ∅ )
62 61 eqeq1d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ∅ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) )
63 simpl ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → 𝐵 ∈ 𝑆 )
64 63 con3i ⊢ ( ¬ 𝐵 ∈ 𝑆 → ¬ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) )
65 2 ndmov ⊢ ( ¬ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐵 + 𝐶 ) = ∅ )
66 64 65 syl ⊢ ( ¬ 𝐵 ∈ 𝑆 → ( 𝐵 + 𝐶 ) = ∅ )
67 66 adantl ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( 𝐵 + 𝐶 ) = ∅ )
68 67 eqeq2d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ↔ ( 𝐴 + 𝐷 ) = ∅ ) )
69 54 62 68 3bitr4d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )
70 28 69 pm2.61dan ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )