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 ( ( 𝐴𝑆𝐶𝑆 ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] = [ ⟨ 𝐶 , 𝐷 ⟩ ] ↔ ( 𝐴 + 𝐷 ) = ( 𝐵 + 𝐶 ) ) )