| Step | Hyp | Ref
| Expression |
| 1 | | dfqs2 42278 |
. 2
⊢ (𝐴 / ∼ ) = ran (𝑎 ∈ 𝐴 ↦ [𝑎] ∼ ) |
| 2 | | qsalrel.2 |
. . . . . . 7
⊢ (𝜑 → ∼ Er 𝐴) |
| 3 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∼ Er 𝐴) |
| 4 | | qsalrel.1 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∼ 𝑦) |
| 5 | 4 | ralrimivva 3202 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦) |
| 6 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦) |
| 7 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
| 8 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (𝑥 ∼ 𝑦 ↔ 𝑎 ∼ 𝑦)) |
| 9 | 8 | ralbidv 3178 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦)) |
| 10 | 9 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = 𝑎) → (∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦)) |
| 11 | 7, 10 | rspcdv 3614 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 → ∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦)) |
| 12 | | qsalrel.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ 𝐴) |
| 13 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑁 → (𝑎 ∼ 𝑦 ↔ 𝑎 ∼ 𝑁)) |
| 14 | 13 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = 𝑁) → (𝑎 ∼ 𝑦 ↔ 𝑎 ∼ 𝑁)) |
| 15 | 12, 14 | rspcdv 3614 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦 → 𝑎 ∼ 𝑁)) |
| 16 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 𝑎 ∼ 𝑦 → 𝑎 ∼ 𝑁)) |
| 17 | 11, 16 | syld 47 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 → 𝑎 ∼ 𝑁)) |
| 18 | 6, 17 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∼ 𝑁) |
| 19 | 3, 18 | erthi 8798 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → [𝑎] ∼ = [𝑁] ∼ ) |
| 20 | 19 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ 𝐴 ↦ [𝑎] ∼ ) = (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ )) |
| 21 | 20 | rneqd 5949 |
. . 3
⊢ (𝜑 → ran (𝑎 ∈ 𝐴 ↦ [𝑎] ∼ ) = ran (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ )) |
| 22 | | eqid 2737 |
. . . 4
⊢ (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ ) = (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ ) |
| 23 | 12 | ne0d 4342 |
. . . 4
⊢ (𝜑 → 𝐴 ≠ ∅) |
| 24 | 22, 23 | rnmptc 7227 |
. . 3
⊢ (𝜑 → ran (𝑎 ∈ 𝐴 ↦ [𝑁] ∼ ) = {[𝑁] ∼ }) |
| 25 | 2 | ecss 8793 |
. . . . 5
⊢ (𝜑 → [𝑁] ∼ ⊆ 𝐴) |
| 26 | 3, 18 | ersym 8757 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑁 ∼ 𝑎) |
| 27 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑁 ∈ 𝐴) |
| 28 | | elecg 8789 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑁 ∈ 𝐴) → (𝑎 ∈ [𝑁] ∼ ↔ 𝑁 ∼ 𝑎)) |
| 29 | 7, 27, 28 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ [𝑁] ∼ ↔ 𝑁 ∼ 𝑎)) |
| 30 | 26, 29 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ [𝑁] ∼ ) |
| 31 | 25, 30 | eqelssd 4005 |
. . . 4
⊢ (𝜑 → [𝑁] ∼ = 𝐴) |
| 32 | 31 | sneqd 4638 |
. . 3
⊢ (𝜑 → {[𝑁] ∼ } = {𝐴}) |
| 33 | 21, 24, 32 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → ran (𝑎 ∈ 𝐴 ↦ [𝑎] ∼ ) = {𝐴}) |
| 34 | 1, 33 | eqtrid 2789 |
1
⊢ (𝜑 → (𝐴 / ∼ ) = {𝐴}) |