This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qsalrel

Description: The quotient set is equal to the singleton of A when all elements are related and A is nonempty. (Contributed by SN, 8-Jun-2023)

Ref Expression
Hypotheses qsalrel.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∼ 𝑦 )
qsalrel.2 ⊢ ( 𝜑 → ∼ Er 𝐴 )
qsalrel.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝐴 )
Assertion qsalrel ( 𝜑 → ( 𝐴 / ∼ ) = { 𝐴 } )

Proof

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 eqtrid ⊢ ( 𝜑 → ( 𝐴 / ∼ ) = { 𝐴 } )