Step | Hyp | Ref
| Expression |
1 | | dfqs2 39778 |
. 2
⊢ (𝐴 / ∼ ) = ran (𝑎 ∈ 𝐴 ↦ [𝑎] ∼ ) |
2 | | qsalrel.2 |
. . . . . . 7
⊢ (𝜑 → ∼ Er 𝐴) |
3 | 2 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∼ Er 𝐴) |
4 | | qsalrel.1 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∼ 𝑦) |
5 | 4 | ralrimivva 3103 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦) |
6 | 5 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦) |
7 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
8 | | breq1 5030 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (𝑥 ∼ 𝑦 ↔ 𝑎 ∼ 𝑦)) |
9 | 8 | ralbidv 3109 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦)) |
10 | 9 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = 𝑎) → (∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦)) |
11 | 7, 10 | rspcdv 3516 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 → ∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦)) |
12 | | qsalrel.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ 𝐴) |
13 | | breq2 5031 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑁 → (𝑎 ∼ 𝑦 ↔ 𝑎 ∼ 𝑁)) |
14 | 13 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = 𝑁) → (𝑎 ∼ 𝑦 ↔ 𝑎 ∼ 𝑁)) |
15 | 12, 14 | rspcdv 3516 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦 → 𝑎 ∼ 𝑁)) |
16 | 15 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦 → 𝑎 ∼ 𝑁)) |
17 | 11, 16 | syld 47 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 → 𝑎 ∼ 𝑁)) |
18 | 6, 17 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∼ 𝑁) |
19 | 3, 18 | erthi 8364 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → [𝑎] ∼ = [𝑁] ∼ ) |
20 | 19 | mpteq2dva 5122 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ 𝐴 ↦ [𝑎] ∼ ) = (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ )) |
21 | 20 | rneqd 5775 |
. . 3
⊢ (𝜑 → ran (𝑎 ∈ 𝐴 ↦ [𝑎] ∼ ) = ran (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ )) |
22 | | eqid 2738 |
. . . 4
⊢ (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ ) = (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ ) |
23 | 12 | ne0d 4222 |
. . . 4
⊢ (𝜑 → 𝐴 ≠ ∅) |
24 | 22, 23 | rnmptc 6973 |
. . 3
⊢ (𝜑 → ran (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ ) = {[𝑁] ∼ }) |
25 | 2 | ecss 8359 |
. . . . 5
⊢ (𝜑 → [𝑁] ∼ ⊆ 𝐴) |
26 | 3, 18 | ersym 8325 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑁 ∼ 𝑎) |
27 | 12 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑁 ∈ 𝐴) |
28 | | elecg 8356 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑁 ∈ 𝐴) → (𝑎 ∈ [𝑁] ∼ ↔ 𝑁 ∼ 𝑎)) |
29 | 7, 27, 28 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ [𝑁] ∼ ↔ 𝑁 ∼ 𝑎)) |
30 | 26, 29 | mpbird 260 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ [𝑁] ∼ ) |
31 | 25, 30 | eqelssd 3896 |
. . . 4
⊢ (𝜑 → [𝑁] ∼ = 𝐴) |
32 | 31 | sneqd 4525 |
. . 3
⊢ (𝜑 → {[𝑁] ∼ } = {𝐴}) |
33 | 21, 24, 32 | 3eqtrd 2777 |
. 2
⊢ (𝜑 → ran (𝑎 ∈ 𝐴 ↦ [𝑎] ∼ ) = {𝐴}) |
34 | 1, 33 | syl5eq 2785 |
1
⊢ (𝜑 → (𝐴 / ∼ ) = {𝐴}) |