Step | Hyp | Ref
| Expression |
1 | | opelxpi 5671 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ⟨𝐴, 𝐵⟩ ∈ (𝑆 × 𝑆)) |
2 | 1 | ad2antrr 725 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) →
⟨𝐴, 𝐵⟩ ∈ (𝑆 × 𝑆)) |
3 | | eceqoveq.5 |
. . . . . . . . 9
⊢ ∼ Er
(𝑆 × 𝑆) |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) → ∼ Er
(𝑆 × 𝑆)) |
5 | | simpr 486 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) →
[⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) |
6 | 4, 5 | ereldm 8697 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) →
(⟨𝐴, 𝐵⟩ ∈ (𝑆 × 𝑆) ↔ ⟨𝐶, 𝐷⟩ ∈ (𝑆 × 𝑆))) |
7 | 2, 6 | mpbid 231 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) →
⟨𝐶, 𝐷⟩ ∈ (𝑆 × 𝑆)) |
8 | | opelxp2 5676 |
. . . . . 6
⊢
(⟨𝐶, 𝐷⟩ ∈ (𝑆 × 𝑆) → 𝐷 ∈ 𝑆) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) ∧ [⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) → 𝐷 ∈ 𝑆) |
10 | 9 | ex 414 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ → 𝐷 ∈ 𝑆)) |
11 | | eceqoveq.9 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) |
12 | 11 | caovcl 7549 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐵 + 𝐶) ∈ 𝑆) |
13 | | eleq1 2826 |
. . . . . . 7
⊢ ((𝐴 + 𝐷) = (𝐵 + 𝐶) → ((𝐴 + 𝐷) ∈ 𝑆 ↔ (𝐵 + 𝐶) ∈ 𝑆)) |
14 | 12, 13 | syl5ibr 246 |
. . . . . 6
⊢ ((𝐴 + 𝐷) = (𝐵 + 𝐶) → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 + 𝐷) ∈ 𝑆)) |
15 | | eceqoveq.7 |
. . . . . . . 8
⊢ dom + = (𝑆 × 𝑆) |
16 | | eceqoveq.8 |
. . . . . . . 8
⊢ ¬
∅ ∈ 𝑆 |
17 | 15, 16 | ndmovrcl 7541 |
. . . . . . 7
⊢ ((𝐴 + 𝐷) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
18 | 17 | simprd 497 |
. . . . . 6
⊢ ((𝐴 + 𝐷) ∈ 𝑆 → 𝐷 ∈ 𝑆) |
19 | 14, 18 | syl6com 37 |
. . . . 5
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴 + 𝐷) = (𝐵 + 𝐶) → 𝐷 ∈ 𝑆)) |
20 | 19 | adantll 713 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → ((𝐴 + 𝐷) = (𝐵 + 𝐶) → 𝐷 ∈ 𝑆)) |
21 | 3 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ∼ Er (𝑆 × 𝑆)) |
22 | 1 | adantr 482 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ⟨𝐴, 𝐵⟩ ∈ (𝑆 × 𝑆)) |
23 | 21, 22 | erth 8698 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩ ∼ ⟨𝐶, 𝐷⟩ ↔ [⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ )) |
24 | | eceqoveq.10 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩ ∼ ⟨𝐶, 𝐷⟩ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
25 | 23, 24 | bitr3d 281 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
26 | 25 | expr 458 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → (𝐷 ∈ 𝑆 → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))) |
27 | 10, 20, 26 | pm5.21ndd 381 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
28 | 27 | an32s 651 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ 𝐵 ∈ 𝑆) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
29 | | eqcom 2744 |
. . . 4
⊢ (∅
= [⟨𝐶, 𝐷⟩] ∼ ↔ [⟨𝐶, 𝐷⟩] ∼ =
∅) |
30 | | erdm 8659 |
. . . . . . . . . . . 12
⊢ ( ∼ Er
(𝑆 × 𝑆) → dom ∼ = (𝑆 × 𝑆)) |
31 | 3, 30 | ax-mp 5 |
. . . . . . . . . . 11
⊢ dom ∼ =
(𝑆 × 𝑆) |
32 | 31 | eleq2i 2830 |
. . . . . . . . . 10
⊢
(⟨𝐶, 𝐷⟩ ∈ dom ∼ ↔
⟨𝐶, 𝐷⟩ ∈ (𝑆 × 𝑆)) |
33 | | ecdmn0 8696 |
. . . . . . . . . 10
⊢
(⟨𝐶, 𝐷⟩ ∈ dom ∼ ↔
[⟨𝐶, 𝐷⟩] ∼ ≠
∅) |
34 | | opelxp 5670 |
. . . . . . . . . 10
⊢
(⟨𝐶, 𝐷⟩ ∈ (𝑆 × 𝑆) ↔ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
35 | 32, 33, 34 | 3bitr3i 301 |
. . . . . . . . 9
⊢
([⟨𝐶, 𝐷⟩] ∼ ≠ ∅ ↔
(𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) |
36 | 35 | simplbi2 502 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑆 → (𝐷 ∈ 𝑆 → [⟨𝐶, 𝐷⟩] ∼ ≠
∅)) |
37 | 36 | ad2antlr 726 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (𝐷 ∈ 𝑆 → [⟨𝐶, 𝐷⟩] ∼ ≠
∅)) |
38 | 37 | necon2bd 2960 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([⟨𝐶, 𝐷⟩] ∼ = ∅ →
¬ 𝐷 ∈ 𝑆)) |
39 | | simpr 486 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝐷 ∈ 𝑆) |
40 | 15 | ndmov 7539 |
. . . . . . 7
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → (𝐴 + 𝐷) = ∅) |
41 | 39, 40 | nsyl5 159 |
. . . . . 6
⊢ (¬
𝐷 ∈ 𝑆 → (𝐴 + 𝐷) = ∅) |
42 | 38, 41 | syl6 35 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([⟨𝐶, 𝐷⟩] ∼ = ∅ →
(𝐴 + 𝐷) = ∅)) |
43 | | eleq1 2826 |
. . . . . . 7
⊢ ((𝐴 + 𝐷) = ∅ → ((𝐴 + 𝐷) ∈ 𝑆 ↔ ∅ ∈ 𝑆)) |
44 | 16, 43 | mtbiri 327 |
. . . . . 6
⊢ ((𝐴 + 𝐷) = ∅ → ¬ (𝐴 + 𝐷) ∈ 𝑆) |
45 | 35 | simprbi 498 |
. . . . . . . 8
⊢
([⟨𝐶, 𝐷⟩] ∼ ≠ ∅ →
𝐷 ∈ 𝑆) |
46 | 11 | caovcl 7549 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → (𝐴 + 𝐷) ∈ 𝑆) |
47 | 46 | ex 414 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑆 → (𝐷 ∈ 𝑆 → (𝐴 + 𝐷) ∈ 𝑆)) |
48 | 47 | ad2antrr 725 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (𝐷 ∈ 𝑆 → (𝐴 + 𝐷) ∈ 𝑆)) |
49 | 45, 48 | syl5 34 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([⟨𝐶, 𝐷⟩] ∼ ≠ ∅ →
(𝐴 + 𝐷) ∈ 𝑆)) |
50 | 49 | necon1bd 2962 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (¬ (𝐴 + 𝐷) ∈ 𝑆 → [⟨𝐶, 𝐷⟩] ∼ =
∅)) |
51 | 44, 50 | syl5 34 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ((𝐴 + 𝐷) = ∅ → [⟨𝐶, 𝐷⟩] ∼ =
∅)) |
52 | 42, 51 | impbid 211 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([⟨𝐶, 𝐷⟩] ∼ = ∅ ↔
(𝐴 + 𝐷) = ∅)) |
53 | 29, 52 | bitrid 283 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (∅ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = ∅)) |
54 | 31 | eleq2i 2830 |
. . . . . . . 8
⊢
(⟨𝐴, 𝐵⟩ ∈ dom ∼ ↔
⟨𝐴, 𝐵⟩ ∈ (𝑆 × 𝑆)) |
55 | | ecdmn0 8696 |
. . . . . . . 8
⊢
(⟨𝐴, 𝐵⟩ ∈ dom ∼ ↔
[⟨𝐴, 𝐵⟩] ∼ ≠
∅) |
56 | | opelxp 5670 |
. . . . . . . 8
⊢
(⟨𝐴, 𝐵⟩ ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
57 | 54, 55, 56 | 3bitr3i 301 |
. . . . . . 7
⊢
([⟨𝐴, 𝐵⟩] ∼ ≠ ∅ ↔
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
58 | 57 | simprbi 498 |
. . . . . 6
⊢
([⟨𝐴, 𝐵⟩] ∼ ≠ ∅ →
𝐵 ∈ 𝑆) |
59 | 58 | necon1bi 2973 |
. . . . 5
⊢ (¬
𝐵 ∈ 𝑆 → [⟨𝐴, 𝐵⟩] ∼ =
∅) |
60 | 59 | adantl 483 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → [⟨𝐴, 𝐵⟩] ∼ =
∅) |
61 | 60 | eqeq1d 2739 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ ∅ =
[⟨𝐶, 𝐷⟩] ∼ )) |
62 | | simpl 484 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝐵 ∈ 𝑆) |
63 | 15 | ndmov 7539 |
. . . . . 6
⊢ (¬
(𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐵 + 𝐶) = ∅) |
64 | 62, 63 | nsyl5 159 |
. . . . 5
⊢ (¬
𝐵 ∈ 𝑆 → (𝐵 + 𝐶) = ∅) |
65 | 64 | adantl 483 |
. . . 4
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → (𝐵 + 𝐶) = ∅) |
66 | 65 | eqeq2d 2748 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ((𝐴 + 𝐷) = (𝐵 + 𝐶) ↔ (𝐴 + 𝐷) = ∅)) |
67 | 53, 61, 66 | 3bitr4d 311 |
. 2
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ ¬ 𝐵 ∈ 𝑆) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
68 | 28, 67 | pm2.61dan 812 |
1
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |