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 2 ndmov ⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → ( 𝐴 + 𝐷 ) = ∅ )
41 39 40 nsyl5 ⊢ ( ¬ 𝐷 ∈ 𝑆 → ( 𝐴 + 𝐷 ) = ∅ )
42 38 41 syl6 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ → ( 𝐴 + 𝐷 ) = ∅ ) )
43 eleq1 ⊢ ( ( 𝐴 + 𝐷 ) = ∅ → ( ( 𝐴 + 𝐷 ) ∈ 𝑆 ↔ ∅ ∈ 𝑆 ) )
44 3 43 mtbiri ⊢ ( ( 𝐴 + 𝐷 ) = ∅ → ¬ ( 𝐴 + 𝐷 ) ∈ 𝑆 )
45 35 simprbi ⊢ ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ≠ ∅ → 𝐷 ∈ 𝑆 )
46 4 caovcl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → ( 𝐴 + 𝐷 ) ∈ 𝑆 )
47 46 ex ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐷 ∈ 𝑆 → ( 𝐴 + 𝐷 ) ∈ 𝑆 ) )
48 47 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( 𝐷 ∈ 𝑆 → ( 𝐴 + 𝐷 ) ∈ 𝑆 ) )
49 45 48 syl5 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ≠ ∅ → ( 𝐴 + 𝐷 ) ∈ 𝑆 ) )
50 49 necon1bd ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( ¬ ( 𝐴 + 𝐷 ) ∈ 𝑆 → [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ ) )
51 44 50 syl5 ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 + 𝐷 ) = ∅ → [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ ) )
52 42 51 impbid ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ = ∅ ↔ ( 𝐴 + 𝐷 ) = ∅ ) )
53 29 52 syl5bb ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( ∅ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ∅ ) )
54 31 eleq2i ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ∼ ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) )
55 ecdmn0 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ∼ ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≠ ∅ )
56 opelxp ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
57 54 55 56 3bitr3i ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≠ ∅ ↔ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
58 57 simprbi ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ≠ ∅ → 𝐵 ∈ 𝑆 )
59 58 necon1bi ⊢ ( ¬ 𝐵 ∈ 𝑆 → [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = ∅ )
60 59 adantl ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = ∅ )
61 60 eqeq1d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ∅ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ) )
62 simpl ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → 𝐵 ∈ 𝑆 )
63 2 ndmov ⊢ ( ¬ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐵 + 𝐶 ) = ∅ )
64 62 63 nsyl5 ⊢ ( ¬ 𝐵 ∈ 𝑆 → ( 𝐵 + 𝐶 ) = ∅ )
65 64 adantl ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( 𝐵 + 𝐶 ) = ∅ )
66 65 eqeq2d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ↔ ( 𝐴 + 𝐷 ) = ∅ ) )
67 53 61 66 3bitr4d ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ¬ 𝐵 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )
68 28 67 pm2.61dan ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ = [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )