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