Metamath Proof Explorer

Theorem releldmqs

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

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

Proof

Step Hyp Ref Expression
1 resdm 
 |-  ( Rel R -> ( R |` dom R ) = R )
2 1 dmqseqd 
 |-  ( Rel R -> ( dom ( R |` dom R ) /. ( R |` dom R ) ) = ( dom R /. R ) )
3 2 eleq2d 
 |-  ( Rel R -> ( A e. ( dom ( R |` dom R ) /. ( R |` dom R ) ) <-> A e. ( dom R /. R ) ) )
4 3 adantl 
 |-  ( ( A e. V /\ Rel R ) -> ( A e. ( dom ( R |` dom R ) /. ( R |` dom R ) ) <-> A e. ( dom R /. R ) ) )
5 eldmqsres2 
 |-  ( A e. V -> ( A e. ( dom ( R |` dom R ) /. ( R |` dom R ) ) <-> E. u e. dom R E. x e. [ u ] R A = [ u ] R ) )
6 5 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 = [ u ] R ) )
7 4 6 bitr3d 
 |-  ( ( A e. V /\ Rel R ) -> ( A e. ( dom R /. R ) <-> E. u e. dom R E. x e. [ u ] R A = [ u ] R ) )
8 7 ex 
 |-  ( A e. V -> ( Rel R -> ( A e. ( dom R /. R ) <-> E. u e. dom R E. x e. [ u ] R A = [ u ] R ) ) )