Metamath Proof Explorer

Theorem releldmqscoss

Description: Elementhood in the domain quotient of the class of cosets by a relation. (Contributed by Peter Mazsa, 23-Apr-2021)

Ref Expression
Assertion releldmqscoss 
|- ( A e. V -> ( Rel R -> ( A e. ( dom ,~ R /. ,~ R ) <-> E. u e. dom R E. x e. [ u ] R A = [ x ] ,~ R ) ) )

Proof

Step Hyp Ref Expression
1 eldmqs1cossres 
 |-  ( A e. V -> ( A e. ( dom ,~ ( R |` dom R ) /. ,~ ( R |` dom R ) ) <-> E. u e. dom R E. x e. [ u ] R A = [ x ] ,~ ( R |` dom R ) ) )
2 1 adantr 
 |-  ( ( A e. V /\ Rel R ) -> ( A e. ( dom ,~ ( R |` dom R ) /. ,~ ( R |` dom R ) ) <-> E. u e. dom R E. x e. [ u ] R A = [ x ] ,~ ( R |` dom R ) ) )
3 resdm 
 |-  ( Rel R -> ( R |` dom R ) = R )
4 3 cosseqd 
 |-  ( Rel R -> ,~ ( R |` dom R ) = ,~ R )
5 4 dmqseqd 
 |-  ( Rel R -> ( dom ,~ ( R |` dom R ) /. ,~ ( R |` dom R ) ) = ( dom ,~ R /. ,~ R ) )
6 5 eleq2d 
 |-  ( Rel R -> ( A e. ( dom ,~ ( R |` dom R ) /. ,~ ( R |` dom R ) ) <-> A e. ( dom ,~ R /. ,~ R ) ) )
7 6 adantl 
 |-  ( ( A e. V /\ Rel R ) -> ( A e. ( dom ,~ ( R |` dom R ) /. ,~ ( R |` dom R ) ) <-> A e. ( dom ,~ R /. ,~ R ) ) )
8 4 eceq2d 
 |-  ( Rel R -> [ x ] ,~ ( R |` dom R ) = [ x ] ,~ R )
9 8 eqeq2d 
 |-  ( Rel R -> ( A = [ x ] ,~ ( R |` dom R ) <-> A = [ x ] ,~ R ) )
10 9 2rexbidv 
 |-  ( Rel R -> ( E. u e. dom R E. x e. [ u ] R A = [ x ] ,~ ( R |` dom R ) <-> E. u e. dom R E. x e. [ u ] R A = [ x ] ,~ R ) )
11 10 adantl 
 |-  ( ( A e. V /\ Rel R ) -> ( E. u e. dom R E. x e. [ u ] R A = [ x ] ,~ ( R |` dom R ) <-> E. u e. dom R E. x e. [ u ] R A = [ x ] ,~ R ) )
12 2 7 11 3bitr3d 
 |-  ( ( A e. V /\ Rel R ) -> ( A e. ( dom ,~ R /. ,~ R ) <-> E. u e. dom R E. x e. [ u ] R A = [ x ] ,~ R ) )
13 12 ex 
 |-  ( A e. V -> ( Rel R -> ( A e. ( dom ,~ R /. ,~ R ) <-> E. u e. dom R E. x e. [ u ] R A = [ x ] ,~ R ) ) )