Proof of Theorem eceqoveq
Step | Hyp | Ref
| Expression |
1 | | opelxpi 5554 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
2 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) →
〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
3 | | eceqoveq.5 |
. . . . . . . . 9
⊢ ∼ Er
(𝑆 × 𝑆) |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → ∼ Er
(𝑆 × 𝑆)) |
5 | | simpr 489 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) →
[〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) |
6 | 4, 5 | ereldm 8340 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) →
(〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ↔ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆))) |
7 | 2, 6 | mpbid 235 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) →
〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) |
8 | | opelxp2 5559 |
. . . . . 6
⊢
(〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆) → 𝐷 ∈ 𝑆) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → 𝐷 ∈ 𝑆) |
10 | 9 | ex 417 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ → 𝐷 ∈ 𝑆)) |
11 | | eceqoveq.9 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) |
12 | 11 | caovcl 7331 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐵 + 𝐶) ∈ 𝑆) |
13 | | eleq1 2838 |
. . . . . . 7
⊢ ((𝐴 + 𝐷) = (𝐵 + 𝐶) → ((𝐴 + 𝐷) ∈ 𝑆 ↔ (𝐵 + 𝐶) ∈ 𝑆)) |
14 | 12, 13 | syl5ibr 249 |
. . . . . 6
⊢ ((𝐴 + 𝐷) = (𝐵 + 𝐶) → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 + 𝐷) ∈ 𝑆)) |
15 | | eceqoveq.7 |
. . . . . . . 8
⊢ dom + = (𝑆 × 𝑆) |
16 | | eceqoveq.8 |
. . . . . . . 8
⊢ ¬
∅ ∈ 𝑆 |
17 | 15, 16 | ndmovrcl 7323 |
. . . . . . 7
⊢ ((𝐴 + 𝐷) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
18 | 17 | simprd 500 |
. . . . . 6
⊢ ((𝐴 + 𝐷) ∈ 𝑆 → 𝐷 ∈ 𝑆) |
19 | 14, 18 | syl6com 37 |
. . . . 5
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴 + 𝐷) = (𝐵 + 𝐶) → 𝐷 ∈ 𝑆)) |
20 | 19 | adantll 714 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → ((𝐴 + 𝐷) = (𝐵 + 𝐶) → 𝐷 ∈ 𝑆)) |
21 | 3 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ∼ Er (𝑆 × 𝑆)) |
22 | 1 | adantr 485 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
23 | 21, 22 | erth 8341 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 ∼ 〈𝐶, 𝐷〉 ↔ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ )) |
24 | | eceqoveq.10 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 ∼ 〈𝐶, 𝐷〉 ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
25 | 23, 24 | bitr3d 284 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
26 | 25 | expr 461 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → (𝐷 ∈ 𝑆 → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))) |
27 | 10, 20, 26 | pm5.21ndd 385 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
28 | 27 | an32s 652 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ 𝐵 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
29 | | eqcom 2766 |
. . . 4
⊢ (∅
= [〈𝐶, 𝐷〉] ∼ ↔ [〈𝐶, 𝐷〉] ∼ =
∅) |
30 | | erdm 8302 |
. . . . . . . . . . . 12
⊢ ( ∼ Er
(𝑆 × 𝑆) → dom ∼ = (𝑆 × 𝑆)) |
31 | 3, 30 | ax-mp 5 |
. . . . . . . . . . 11
⊢ dom ∼ =
(𝑆 × 𝑆) |
32 | 31 | eleq2i 2842 |
. . . . . . . . . 10
⊢
(〈𝐶, 𝐷〉 ∈ dom ∼ ↔
〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) |
33 | | ecdmn0 8339 |
. . . . . . . . . 10
⊢
(〈𝐶, 𝐷〉 ∈ dom ∼ ↔
[〈𝐶, 𝐷〉] ∼ ≠
∅) |
34 | | opelxp 5553 |
. . . . . . . . . 10
⊢
(〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆) ↔ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
35 | 32, 33, 34 | 3bitr3i 305 |
. . . . . . . . 9
⊢
([〈𝐶, 𝐷〉] ∼ ≠ ∅ ↔
(𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
36 | 35 | simplbi2 505 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑆 → (𝐷 ∈ 𝑆 → [〈𝐶, 𝐷〉] ∼ ≠
∅)) |
37 | 36 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (𝐷 ∈ 𝑆 → [〈𝐶, 𝐷〉] ∼ ≠
∅)) |
38 | 37 | necon2bd 2965 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐶, 𝐷〉] ∼ = ∅ →
¬ 𝐷 ∈ 𝑆)) |
39 | | simpr 489 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝐷 ∈ 𝑆) |
40 | 15 | ndmov 7321 |
. . . . . . 7
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → (𝐴 + 𝐷) = ∅) |
41 | 39, 40 | nsyl5 162 |
. . . . . 6
⊢ (¬
𝐷 ∈ 𝑆 → (𝐴 + 𝐷) = ∅) |
42 | 38, 41 | syl6 35 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐶, 𝐷〉] ∼ = ∅ →
(𝐴 + 𝐷) = ∅)) |
43 | | eleq1 2838 |
. . . . . . 7
⊢ ((𝐴 + 𝐷) = ∅ → ((𝐴 + 𝐷) ∈ 𝑆 ↔ ∅ ∈ 𝑆)) |
44 | 16, 43 | mtbiri 331 |
. . . . . 6
⊢ ((𝐴 + 𝐷) = ∅ → ¬ (𝐴 + 𝐷) ∈ 𝑆) |
45 | 35 | simprbi 501 |
. . . . . . . 8
⊢
([〈𝐶, 𝐷〉] ∼ ≠ ∅ →
𝐷 ∈ 𝑆) |
46 | 11 | caovcl 7331 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → (𝐴 + 𝐷) ∈ 𝑆) |
47 | 46 | ex 417 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑆 → (𝐷 ∈ 𝑆 → (𝐴 + 𝐷) ∈ 𝑆)) |
48 | 47 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (𝐷 ∈ 𝑆 → (𝐴 + 𝐷) ∈ 𝑆)) |
49 | 45, 48 | syl5 34 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐶, 𝐷〉] ∼ ≠ ∅ →
(𝐴 + 𝐷) ∈ 𝑆)) |
50 | 49 | necon1bd 2967 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (¬ (𝐴 + 𝐷) ∈ 𝑆 → [〈𝐶, 𝐷〉] ∼ =
∅)) |
51 | 44, 50 | syl5 34 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ((𝐴 + 𝐷) = ∅ → [〈𝐶, 𝐷〉] ∼ =
∅)) |
52 | 42, 51 | impbid 215 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐶, 𝐷〉] ∼ = ∅ ↔
(𝐴 + 𝐷) = ∅)) |
53 | 29, 52 | syl5bb 286 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (∅ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = ∅)) |
54 | 31 | eleq2i 2842 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ dom ∼ ↔
〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
55 | | ecdmn0 8339 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ dom ∼ ↔
[〈𝐴, 𝐵〉] ∼ ≠
∅) |
56 | | opelxp 5553 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
57 | 54, 55, 56 | 3bitr3i 305 |
. . . . . . 7
⊢
([〈𝐴, 𝐵〉] ∼ ≠ ∅ ↔
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
58 | 57 | simprbi 501 |
. . . . . 6
⊢
([〈𝐴, 𝐵〉] ∼ ≠ ∅ →
𝐵 ∈ 𝑆) |
59 | 58 | necon1bi 2977 |
. . . . 5
⊢ (¬
𝐵 ∈ 𝑆 → [〈𝐴, 𝐵〉] ∼ =
∅) |
60 | 59 | adantl 486 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → [〈𝐴, 𝐵〉] ∼ =
∅) |
61 | 60 | eqeq1d 2761 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ ∅ =
[〈𝐶, 𝐷〉] ∼ )) |
62 | | simpl 487 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝐵 ∈ 𝑆) |
63 | 15 | ndmov 7321 |
. . . . . 6
⊢ (¬
(𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐵 + 𝐶) = ∅) |
64 | 62, 63 | nsyl5 162 |
. . . . 5
⊢ (¬
𝐵 ∈ 𝑆 → (𝐵 + 𝐶) = ∅) |
65 | 64 | adantl 486 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (𝐵 + 𝐶) = ∅) |
66 | 65 | eqeq2d 2770 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ((𝐴 + 𝐷) = (𝐵 + 𝐶) ↔ (𝐴 + 𝐷) = ∅)) |
67 | 53, 61, 66 | 3bitr4d 315 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
68 | 28, 67 | pm2.61dan 813 |
1
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |