Step |
Hyp |
Ref |
Expression |
1 |
|
qsalrel.1 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∼ 𝑦 ) |
2 |
|
qsalrel.2 |
⊢ ( 𝜑 → ∼ Er 𝐴 ) |
3 |
|
qsalrel.3 |
⊢ ( 𝜑 → 𝑁 ∈ 𝐴 ) |
4 |
|
dfqs2 |
⊢ ( 𝐴 / ∼ ) = ran ( 𝑎 ∈ 𝐴 ↦ [ 𝑎 ] ∼ ) |
5 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∼ Er 𝐴 ) |
6 |
1
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 ) |
7 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 ) |
8 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 ) |
9 |
|
breq1 |
⊢ ( 𝑥 = 𝑎 → ( 𝑥 ∼ 𝑦 ↔ 𝑎 ∼ 𝑦 ) ) |
10 |
9
|
ralbidv |
⊢ ( 𝑥 = 𝑎 → ( ∀ 𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 𝑎 ∼ 𝑦 ) ) |
11 |
10
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 = 𝑎 ) → ( ∀ 𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 𝑎 ∼ 𝑦 ) ) |
12 |
8 11
|
rspcdv |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 → ∀ 𝑦 ∈ 𝐴 𝑎 ∼ 𝑦 ) ) |
13 |
|
breq2 |
⊢ ( 𝑦 = 𝑁 → ( 𝑎 ∼ 𝑦 ↔ 𝑎 ∼ 𝑁 ) ) |
14 |
13
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 = 𝑁 ) → ( 𝑎 ∼ 𝑦 ↔ 𝑎 ∼ 𝑁 ) ) |
15 |
3 14
|
rspcdv |
⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 𝑎 ∼ 𝑦 → 𝑎 ∼ 𝑁 ) ) |
16 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑎 ∼ 𝑦 → 𝑎 ∼ 𝑁 ) ) |
17 |
12 16
|
syld |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ∼ 𝑦 → 𝑎 ∼ 𝑁 ) ) |
18 |
7 17
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∼ 𝑁 ) |
19 |
5 18
|
erthi |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → [ 𝑎 ] ∼ = [ 𝑁 ] ∼ ) |
20 |
19
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 ↦ [ 𝑎 ] ∼ ) = ( 𝑎 ∈ 𝐴 ↦ [ 𝑁 ] ∼ ) ) |
21 |
20
|
rneqd |
⊢ ( 𝜑 → ran ( 𝑎 ∈ 𝐴 ↦ [ 𝑎 ] ∼ ) = ran ( 𝑎 ∈ 𝐴 ↦ [ 𝑁 ] ∼ ) ) |
22 |
|
eqid |
⊢ ( 𝑎 ∈ 𝐴 ↦ [ 𝑁 ] ∼ ) = ( 𝑎 ∈ 𝐴 ↦ [ 𝑁 ] ∼ ) |
23 |
3
|
ne0d |
⊢ ( 𝜑 → 𝐴 ≠ ∅ ) |
24 |
22 23
|
rnmptc |
⊢ ( 𝜑 → ran ( 𝑎 ∈ 𝐴 ↦ [ 𝑁 ] ∼ ) = { [ 𝑁 ] ∼ } ) |
25 |
2
|
ecss |
⊢ ( 𝜑 → [ 𝑁 ] ∼ ⊆ 𝐴 ) |
26 |
5 18
|
ersym |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑁 ∼ 𝑎 ) |
27 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑁 ∈ 𝐴 ) |
28 |
|
elecg |
⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑁 ∈ 𝐴 ) → ( 𝑎 ∈ [ 𝑁 ] ∼ ↔ 𝑁 ∼ 𝑎 ) ) |
29 |
8 27 28
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ∈ [ 𝑁 ] ∼ ↔ 𝑁 ∼ 𝑎 ) ) |
30 |
26 29
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ [ 𝑁 ] ∼ ) |
31 |
25 30
|
eqelssd |
⊢ ( 𝜑 → [ 𝑁 ] ∼ = 𝐴 ) |
32 |
31
|
sneqd |
⊢ ( 𝜑 → { [ 𝑁 ] ∼ } = { 𝐴 } ) |
33 |
21 24 32
|
3eqtrd |
⊢ ( 𝜑 → ran ( 𝑎 ∈ 𝐴 ↦ [ 𝑎 ] ∼ ) = { 𝐴 } ) |
34 |
4 33
|
syl5eq |
⊢ ( 𝜑 → ( 𝐴 / ∼ ) = { 𝐴 } ) |