Proof of Theorem eceqoveq
Step | Hyp | Ref
| Expression |
1 | | opelxpi 5394 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
2 | 1 | ad2antrr 716 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) →
〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
3 | | eceqoveq.5 |
. . . . . . . . 9
⊢ ∼ Er
(𝑆 × 𝑆) |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → ∼ Er
(𝑆 × 𝑆)) |
5 | | simpr 479 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) →
[〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) |
6 | 4, 5 | ereldm 8074 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) →
(〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ↔ 〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆))) |
7 | 2, 6 | mpbid 224 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) →
〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) |
8 | | opelxp2 5399 |
. . . . . 6
⊢
(〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆) → 𝐷 ∈ 𝑆) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → 𝐷 ∈ 𝑆) |
10 | 9 | ex 403 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ → 𝐷 ∈ 𝑆)) |
11 | | eceqoveq.9 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) |
12 | 11 | caovcl 7107 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐵 + 𝐶) ∈ 𝑆) |
13 | | eleq1 2847 |
. . . . . . 7
⊢ ((𝐴 + 𝐷) = (𝐵 + 𝐶) → ((𝐴 + 𝐷) ∈ 𝑆 ↔ (𝐵 + 𝐶) ∈ 𝑆)) |
14 | 12, 13 | syl5ibr 238 |
. . . . . 6
⊢ ((𝐴 + 𝐷) = (𝐵 + 𝐶) → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 + 𝐷) ∈ 𝑆)) |
15 | | eceqoveq.7 |
. . . . . . . 8
⊢ dom + = (𝑆 × 𝑆) |
16 | | eceqoveq.8 |
. . . . . . . 8
⊢ ¬
∅ ∈ 𝑆 |
17 | 15, 16 | ndmovrcl 7099 |
. . . . . . 7
⊢ ((𝐴 + 𝐷) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
18 | 17 | simprd 491 |
. . . . . 6
⊢ ((𝐴 + 𝐷) ∈ 𝑆 → 𝐷 ∈ 𝑆) |
19 | 14, 18 | syl6com 37 |
. . . . 5
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴 + 𝐷) = (𝐵 + 𝐶) → 𝐷 ∈ 𝑆)) |
20 | 19 | adantll 704 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → ((𝐴 + 𝐷) = (𝐵 + 𝐶) → 𝐷 ∈ 𝑆)) |
21 | 3 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ∼ Er (𝑆 × 𝑆)) |
22 | 1 | adantr 474 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
23 | 21, 22 | erth 8075 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 ∼ 〈𝐶, 𝐷〉 ↔ [〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ )) |
24 | | eceqoveq.10 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 ∼ 〈𝐶, 𝐷〉 ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
25 | 23, 24 | bitr3d 273 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
26 | 25 | expr 450 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → (𝐷 ∈ 𝑆 → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))) |
27 | 10, 20, 26 | pm5.21ndd 371 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
28 | 27 | an32s 642 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ 𝐵 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
29 | | eqcom 2785 |
. . . 4
⊢ (∅
= [〈𝐶, 𝐷〉] ∼ ↔ [〈𝐶, 𝐷〉] ∼ =
∅) |
30 | | erdm 8038 |
. . . . . . . . . . . 12
⊢ ( ∼ Er
(𝑆 × 𝑆) → dom ∼ = (𝑆 × 𝑆)) |
31 | 3, 30 | ax-mp 5 |
. . . . . . . . . . 11
⊢ dom ∼ =
(𝑆 × 𝑆) |
32 | 31 | eleq2i 2851 |
. . . . . . . . . 10
⊢
(〈𝐶, 𝐷〉 ∈ dom ∼ ↔
〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆)) |
33 | | ecdmn0 8073 |
. . . . . . . . . 10
⊢
(〈𝐶, 𝐷〉 ∈ dom ∼ ↔
[〈𝐶, 𝐷〉] ∼ ≠
∅) |
34 | | opelxp 5393 |
. . . . . . . . . 10
⊢
(〈𝐶, 𝐷〉 ∈ (𝑆 × 𝑆) ↔ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
35 | 32, 33, 34 | 3bitr3i 293 |
. . . . . . . . 9
⊢
([〈𝐶, 𝐷〉] ∼ ≠ ∅ ↔
(𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
36 | 35 | simplbi2 496 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑆 → (𝐷 ∈ 𝑆 → [〈𝐶, 𝐷〉] ∼ ≠
∅)) |
37 | 36 | ad2antlr 717 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (𝐷 ∈ 𝑆 → [〈𝐶, 𝐷〉] ∼ ≠
∅)) |
38 | 37 | necon2bd 2985 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐶, 𝐷〉] ∼ = ∅ →
¬ 𝐷 ∈ 𝑆)) |
39 | | simpr 479 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝐷 ∈ 𝑆) |
40 | 39 | con3i 152 |
. . . . . . 7
⊢ (¬
𝐷 ∈ 𝑆 → ¬ (𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
41 | 15 | ndmov 7097 |
. . . . . . 7
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → (𝐴 + 𝐷) = ∅) |
42 | 40, 41 | syl 17 |
. . . . . 6
⊢ (¬
𝐷 ∈ 𝑆 → (𝐴 + 𝐷) = ∅) |
43 | 38, 42 | syl6 35 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐶, 𝐷〉] ∼ = ∅ →
(𝐴 + 𝐷) = ∅)) |
44 | | eleq1 2847 |
. . . . . . 7
⊢ ((𝐴 + 𝐷) = ∅ → ((𝐴 + 𝐷) ∈ 𝑆 ↔ ∅ ∈ 𝑆)) |
45 | 16, 44 | mtbiri 319 |
. . . . . 6
⊢ ((𝐴 + 𝐷) = ∅ → ¬ (𝐴 + 𝐷) ∈ 𝑆) |
46 | 35 | simprbi 492 |
. . . . . . . 8
⊢
([〈𝐶, 𝐷〉] ∼ ≠ ∅ →
𝐷 ∈ 𝑆) |
47 | 11 | caovcl 7107 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → (𝐴 + 𝐷) ∈ 𝑆) |
48 | 47 | ex 403 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑆 → (𝐷 ∈ 𝑆 → (𝐴 + 𝐷) ∈ 𝑆)) |
49 | 48 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (𝐷 ∈ 𝑆 → (𝐴 + 𝐷) ∈ 𝑆)) |
50 | 46, 49 | syl5 34 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐶, 𝐷〉] ∼ ≠ ∅ →
(𝐴 + 𝐷) ∈ 𝑆)) |
51 | 50 | necon1bd 2987 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (¬ (𝐴 + 𝐷) ∈ 𝑆 → [〈𝐶, 𝐷〉] ∼ =
∅)) |
52 | 45, 51 | syl5 34 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ((𝐴 + 𝐷) = ∅ → [〈𝐶, 𝐷〉] ∼ =
∅)) |
53 | 43, 52 | impbid 204 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐶, 𝐷〉] ∼ = ∅ ↔
(𝐴 + 𝐷) = ∅)) |
54 | 29, 53 | syl5bb 275 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (∅ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = ∅)) |
55 | 31 | eleq2i 2851 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ dom ∼ ↔
〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) |
56 | | ecdmn0 8073 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ dom ∼ ↔
[〈𝐴, 𝐵〉] ∼ ≠
∅) |
57 | | opelxp 5393 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
58 | 55, 56, 57 | 3bitr3i 293 |
. . . . . . 7
⊢
([〈𝐴, 𝐵〉] ∼ ≠ ∅ ↔
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
59 | 58 | simprbi 492 |
. . . . . 6
⊢
([〈𝐴, 𝐵〉] ∼ ≠ ∅ →
𝐵 ∈ 𝑆) |
60 | 59 | necon1bi 2997 |
. . . . 5
⊢ (¬
𝐵 ∈ 𝑆 → [〈𝐴, 𝐵〉] ∼ =
∅) |
61 | 60 | adantl 475 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → [〈𝐴, 𝐵〉] ∼ =
∅) |
62 | 61 | eqeq1d 2780 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ ∅ =
[〈𝐶, 𝐷〉] ∼ )) |
63 | | simpl 476 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝐵 ∈ 𝑆) |
64 | 63 | con3i 152 |
. . . . . 6
⊢ (¬
𝐵 ∈ 𝑆 → ¬ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
65 | 15 | ndmov 7097 |
. . . . . 6
⊢ (¬
(𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐵 + 𝐶) = ∅) |
66 | 64, 65 | syl 17 |
. . . . 5
⊢ (¬
𝐵 ∈ 𝑆 → (𝐵 + 𝐶) = ∅) |
67 | 66 | adantl 475 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (𝐵 + 𝐶) = ∅) |
68 | 67 | eqeq2d 2788 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ((𝐴 + 𝐷) = (𝐵 + 𝐶) ↔ (𝐴 + 𝐷) = ∅)) |
69 | 54, 62, 68 | 3bitr4d 303 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
70 | 28, 69 | pm2.61dan 803 |
1
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ([〈𝐴, 𝐵〉] ∼ = [〈𝐶, 𝐷〉] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |