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 
|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> x .~ y )
qsalrel.2 
|- ( ph -> .~ Er A )
qsalrel.3 
|- ( ph -> N e. A )
Assertion qsalrel 
|- ( ph -> ( A /. .~ ) = { A } )

Proof

Step Hyp Ref Expression
1 qsalrel.1 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> x .~ y )
2 qsalrel.2 
 |-  ( ph -> .~ Er A )
3 qsalrel.3 
 |-  ( ph -> N e. A )
4 dfqs2 
 |-  ( A /. .~ ) = ran ( a e. A |-> [ a ] .~ )
5 2 adantr 
 |-  ( ( ph /\ a e. A ) -> .~ Er A )
6 1 ralrimivva 
 |-  ( ph -> A. x e. A A. y e. A x .~ y )
7 6 adantr 
 |-  ( ( ph /\ a e. A ) -> A. x e. A A. y e. A x .~ y )
8 simpr 
 |-  ( ( ph /\ a e. A ) -> a e. A )
9 breq1 
 |-  ( x = a -> ( x .~ y <-> a .~ y ) )
10 9 ralbidv 
 |-  ( x = a -> ( A. y e. A x .~ y <-> A. y e. A a .~ y ) )
11 10 adantl 
 |-  ( ( ( ph /\ a e. A ) /\ x = a ) -> ( A. y e. A x .~ y <-> A. y e. A a .~ y ) )
12 8 11 rspcdv 
 |-  ( ( ph /\ a e. A ) -> ( A. x e. A A. y e. A x .~ y -> A. y e. A a .~ y ) )
13 breq2 
 |-  ( y = N -> ( a .~ y <-> a .~ N ) )
14 13 adantl 
 |-  ( ( ph /\ y = N ) -> ( a .~ y <-> a .~ N ) )
15 3 14 rspcdv 
 |-  ( ph -> ( A. y e. A a .~ y -> a .~ N ) )
16 15 adantr 
 |-  ( ( ph /\ a e. A ) -> ( A. y e. A a .~ y -> a .~ N ) )
17 12 16 syld 
 |-  ( ( ph /\ a e. A ) -> ( A. x e. A A. y e. A x .~ y -> a .~ N ) )
18 7 17 mpd 
 |-  ( ( ph /\ a e. A ) -> a .~ N )
19 5 18 erthi 
 |-  ( ( ph /\ a e. A ) -> [ a ] .~ = [ N ] .~ )
20 19 mpteq2dva 
 |-  ( ph -> ( a e. A |-> [ a ] .~ ) = ( a e. A |-> [ N ] .~ ) )
21 20 rneqd 
 |-  ( ph -> ran ( a e. A |-> [ a ] .~ ) = ran ( a e. A |-> [ N ] .~ ) )
22 eqid 
 |-  ( a e. A |-> [ N ] .~ ) = ( a e. A |-> [ N ] .~ )
23 3 ne0d 
 |-  ( ph -> A =/= (/) )
24 22 23 rnmptc 
 |-  ( ph -> ran ( a e. A |-> [ N ] .~ ) = { [ N ] .~ } )
25 2 ecss 
 |-  ( ph -> [ N ] .~ C_ A )
26 5 18 ersym 
 |-  ( ( ph /\ a e. A ) -> N .~ a )
27 3 adantr 
 |-  ( ( ph /\ a e. A ) -> N e. A )
28 elecg 
 |-  ( ( a e. A /\ N e. A ) -> ( a e. [ N ] .~ <-> N .~ a ) )
29 8 27 28 syl2anc 
 |-  ( ( ph /\ a e. A ) -> ( a e. [ N ] .~ <-> N .~ a ) )
30 26 29 mpbird 
 |-  ( ( ph /\ a e. A ) -> a e. [ N ] .~ )
31 25 30 eqelssd 
 |-  ( ph -> [ N ] .~ = A )
32 31 sneqd 
 |-  ( ph -> { [ N ] .~ } = { A } )
33 21 24 32 3eqtrd 
 |-  ( ph -> ran ( a e. A |-> [ a ] .~ ) = { A } )
34 4 33 syl5eq 
 |-  ( ph -> ( A /. .~ ) = { A } )