Step | Hyp | Ref
| Expression |
1 | | ee4anv 1927 |
. . . 4
⊢
(∃𝑦∃𝑧∃𝑤∃𝑣(((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ∧ ((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) ↔
(∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ∧
∃𝑤∃𝑣((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼
))) |
2 | | an4 581 |
. . . . . . 7
⊢ ((((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ∧ ((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) ↔ (((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ (𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ )) ∧ (𝑥 = [(𝑦 + 𝑧)] ∼ ∧ 𝑢 = [(𝑤 + 𝑣)] ∼
))) |
3 | | eleq1 2233 |
. . . . . . . . . . . . 13
⊢ (𝐴 = [𝑦] ∼ → (𝐴 ∈ (𝑆 / ∼ ) ↔ [𝑦] ∼ ∈ (𝑆 / ∼
))) |
4 | | eleq1 2233 |
. . . . . . . . . . . . 13
⊢ (𝐵 = [𝑧] ∼ → (𝐵 ∈ (𝑆 / ∼ ) ↔ [𝑧] ∼ ∈ (𝑆 / ∼
))) |
5 | 3, 4 | bi2anan9 601 |
. . . . . . . . . . . 12
⊢ ((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) → ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) ↔ ([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼
)))) |
6 | 5 | adantr 274 |
. . . . . . . . . . 11
⊢ (((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ (𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ )) → ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) ↔ ([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼
)))) |
7 | 6 | biimpac 296 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) ∧ ((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ (𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ))) → ([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼
))) |
8 | | eqtr2 2189 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = [𝑦] ∼ ∧ 𝐴 = [𝑤] ∼ ) → [𝑦] ∼ = [𝑤] ∼ ) |
9 | | eqtr2 2189 |
. . . . . . . . . . . . 13
⊢ ((𝐵 = [𝑧] ∼ ∧ 𝐵 = [𝑣] ∼ ) → [𝑧] ∼ = [𝑣] ∼ ) |
10 | 8, 9 | anim12i 336 |
. . . . . . . . . . . 12
⊢ (((𝐴 = [𝑦] ∼ ∧ 𝐴 = [𝑤] ∼ ) ∧ (𝐵 = [𝑧] ∼ ∧ 𝐵 = [𝑣] ∼ )) → ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) |
11 | 10 | an4s 583 |
. . . . . . . . . . 11
⊢ (((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ (𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ )) → ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) |
12 | 11 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) ∧ ((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ (𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ))) → ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) |
13 | | th3qlem1.1 |
. . . . . . . . . . . 12
⊢ ∼ Er
𝑆 |
14 | 13 | a1i 9 |
. . . . . . . . . . 11
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → ∼ Er
𝑆) |
15 | | simprl 526 |
. . . . . . . . . . . . 13
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → [𝑦] ∼ = [𝑤] ∼ ) |
16 | | erdm 6523 |
. . . . . . . . . . . . . . . 16
⊢ ( ∼ Er
𝑆 → dom ∼ =
𝑆) |
17 | 13, 16 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ dom ∼ =
𝑆 |
18 | | simpll 524 |
. . . . . . . . . . . . . . 15
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → [𝑦] ∼ ∈ (𝑆 / ∼ )) |
19 | | ecelqsdm 6583 |
. . . . . . . . . . . . . . 15
⊢ ((dom
∼
= 𝑆 ∧ [𝑦] ∼ ∈ (𝑆 / ∼ )) → 𝑦 ∈ 𝑆) |
20 | 17, 18, 19 | sylancr 412 |
. . . . . . . . . . . . . 14
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → 𝑦 ∈ 𝑆) |
21 | 14, 20 | erth 6557 |
. . . . . . . . . . . . 13
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → (𝑦 ∼ 𝑤 ↔ [𝑦] ∼ = [𝑤] ∼ )) |
22 | 15, 21 | mpbird 166 |
. . . . . . . . . . . 12
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → 𝑦 ∼ 𝑤) |
23 | | simprr 527 |
. . . . . . . . . . . . 13
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → [𝑧] ∼ = [𝑣] ∼ ) |
24 | | simplr 525 |
. . . . . . . . . . . . . . 15
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → [𝑧] ∼ ∈ (𝑆 / ∼ )) |
25 | | ecelqsdm 6583 |
. . . . . . . . . . . . . . 15
⊢ ((dom
∼
= 𝑆 ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) → 𝑧 ∈ 𝑆) |
26 | 17, 24, 25 | sylancr 412 |
. . . . . . . . . . . . . 14
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → 𝑧 ∈ 𝑆) |
27 | 14, 26 | erth 6557 |
. . . . . . . . . . . . 13
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → (𝑧 ∼ 𝑣 ↔ [𝑧] ∼ = [𝑣] ∼ )) |
28 | 23, 27 | mpbird 166 |
. . . . . . . . . . . 12
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → 𝑧 ∼ 𝑣) |
29 | 15, 18 | eqeltrrd 2248 |
. . . . . . . . . . . . . 14
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → [𝑤] ∼ ∈ (𝑆 / ∼ )) |
30 | | ecelqsdm 6583 |
. . . . . . . . . . . . . 14
⊢ ((dom
∼
= 𝑆 ∧ [𝑤] ∼ ∈ (𝑆 / ∼ )) → 𝑤 ∈ 𝑆) |
31 | 17, 29, 30 | sylancr 412 |
. . . . . . . . . . . . 13
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → 𝑤 ∈ 𝑆) |
32 | 23, 24 | eqeltrrd 2248 |
. . . . . . . . . . . . . 14
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → [𝑣] ∼ ∈ (𝑆 / ∼ )) |
33 | | ecelqsdm 6583 |
. . . . . . . . . . . . . 14
⊢ ((dom
∼
= 𝑆 ∧ [𝑣] ∼ ∈ (𝑆 / ∼ )) → 𝑣 ∈ 𝑆) |
34 | 17, 32, 33 | sylancr 412 |
. . . . . . . . . . . . 13
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → 𝑣 ∈ 𝑆) |
35 | | th3qlem1.3 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝑦 ∼ 𝑤 ∧ 𝑧 ∼ 𝑣) → (𝑦 + 𝑧) ∼ (𝑤 + 𝑣))) |
36 | 20, 31, 26, 34, 35 | syl22anc 1234 |
. . . . . . . . . . . 12
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → ((𝑦 ∼ 𝑤 ∧ 𝑧 ∼ 𝑣) → (𝑦 + 𝑧) ∼ (𝑤 + 𝑣))) |
37 | 22, 28, 36 | mp2and 431 |
. . . . . . . . . . 11
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → (𝑦 + 𝑧) ∼ (𝑤 + 𝑣)) |
38 | 14, 37 | erthi 6559 |
. . . . . . . . . 10
⊢ ((([𝑦] ∼ ∈ (𝑆 / ∼ ) ∧ [𝑧] ∼ ∈ (𝑆 / ∼ )) ∧ ([𝑦] ∼ = [𝑤] ∼ ∧ [𝑧] ∼ = [𝑣] ∼ )) → [(𝑦 + 𝑧)] ∼ = [(𝑤 + 𝑣)] ∼ ) |
39 | 7, 12, 38 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) ∧ ((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ (𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ))) → [(𝑦 + 𝑧)] ∼ = [(𝑤 + 𝑣)] ∼ ) |
40 | | eqeq12 2183 |
. . . . . . . . 9
⊢ ((𝑥 = [(𝑦 + 𝑧)] ∼ ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ ) → (𝑥 = 𝑢 ↔ [(𝑦 + 𝑧)] ∼ = [(𝑤 + 𝑣)] ∼ )) |
41 | 39, 40 | syl5ibrcom 156 |
. . . . . . . 8
⊢ (((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) ∧ ((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ (𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ))) → ((𝑥 = [(𝑦 + 𝑧)] ∼ ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ ) → 𝑥 = 𝑢)) |
42 | 41 | expimpd 361 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) → ((((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ (𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ )) ∧ (𝑥 = [(𝑦 + 𝑧)] ∼ ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) → 𝑥 = 𝑢)) |
43 | 2, 42 | syl5bi 151 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) → ((((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ∧ ((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) → 𝑥 = 𝑢)) |
44 | 43 | exlimdvv 1890 |
. . . . 5
⊢ ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) →
(∃𝑤∃𝑣(((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ∧ ((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) → 𝑥 = 𝑢)) |
45 | 44 | exlimdvv 1890 |
. . . 4
⊢ ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) →
(∃𝑦∃𝑧∃𝑤∃𝑣(((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ∧ ((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) → 𝑥 = 𝑢)) |
46 | 1, 45 | syl5bir 152 |
. . 3
⊢ ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) →
((∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ∧
∃𝑤∃𝑣((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) → 𝑥 = 𝑢)) |
47 | 46 | alrimivv 1868 |
. 2
⊢ ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) →
∀𝑥∀𝑢((∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ∧
∃𝑤∃𝑣((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) → 𝑥 = 𝑢)) |
48 | | eqeq1 2177 |
. . . . . 6
⊢ (𝑥 = 𝑢 → (𝑥 = [(𝑦 + 𝑧)] ∼ ↔ 𝑢 = [(𝑦 + 𝑧)] ∼ )) |
49 | 48 | anbi2d 461 |
. . . . 5
⊢ (𝑥 = 𝑢 → (((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ↔ ((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑢 = [(𝑦 + 𝑧)] ∼
))) |
50 | 49 | 2exbidv 1861 |
. . . 4
⊢ (𝑥 = 𝑢 → (∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ↔
∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑢 = [(𝑦 + 𝑧)] ∼
))) |
51 | | eceq1 6548 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → [𝑦] ∼ = [𝑤] ∼ ) |
52 | 51 | eqeq2d 2182 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (𝐴 = [𝑦] ∼ ↔ 𝐴 = [𝑤] ∼ )) |
53 | | eceq1 6548 |
. . . . . . . 8
⊢ (𝑧 = 𝑣 → [𝑧] ∼ = [𝑣] ∼ ) |
54 | 53 | eqeq2d 2182 |
. . . . . . 7
⊢ (𝑧 = 𝑣 → (𝐵 = [𝑧] ∼ ↔ 𝐵 = [𝑣] ∼ )) |
55 | 52, 54 | bi2anan9 601 |
. . . . . 6
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → ((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ↔ (𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼
))) |
56 | | oveq12 5862 |
. . . . . . . 8
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → (𝑦 + 𝑧) = (𝑤 + 𝑣)) |
57 | 56 | eceq1d 6549 |
. . . . . . 7
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → [(𝑦 + 𝑧)] ∼ = [(𝑤 + 𝑣)] ∼ ) |
58 | 57 | eqeq2d 2182 |
. . . . . 6
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → (𝑢 = [(𝑦 + 𝑧)] ∼ ↔ 𝑢 = [(𝑤 + 𝑣)] ∼ )) |
59 | 55, 58 | anbi12d 470 |
. . . . 5
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → (((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑢 = [(𝑦 + 𝑧)] ∼ ) ↔ ((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼
))) |
60 | 59 | cbvex2v 1917 |
. . . 4
⊢
(∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑢 = [(𝑦 + 𝑧)] ∼ ) ↔
∃𝑤∃𝑣((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) |
61 | 50, 60 | bitrdi 195 |
. . 3
⊢ (𝑥 = 𝑢 → (∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ↔
∃𝑤∃𝑣((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼
))) |
62 | 61 | mo4 2080 |
. 2
⊢
(∃*𝑥∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ↔
∀𝑥∀𝑢((∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ ) ∧
∃𝑤∃𝑣((𝐴 = [𝑤] ∼ ∧ 𝐵 = [𝑣] ∼ ) ∧ 𝑢 = [(𝑤 + 𝑣)] ∼ )) → 𝑥 = 𝑢)) |
63 | 47, 62 | sylibr 133 |
1
⊢ ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) →
∃*𝑥∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼ )) |