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

Metamath Proof Explorer

Theorem eceldmqsxrncnvepres2

Description: An ( R |X. (`'E |`A ) ) -coset in its domain quotient. In the pet span ( R |X. (`' E |`A ) ) , a block [ B ] lies in the domain quotient exactly when its representative B belongs to A and actually fires at least one arrow (has some x e. B and some y with B R y ). (Contributed by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion eceldmqsxrncnvepres2 
|- ( ( A e. V /\ B e. W /\ R e. X ) -> ( [ B ] ( R |X. ( `' _E |` A ) ) e. ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) <-> ( B e. A /\ E. x x e. B /\ E. y B R y ) ) )

Proof

Step Hyp Ref Expression
1 xrncnvepresex 
 |-  ( ( A e. V /\ R e. X ) -> ( R |X. ( `' _E |` A ) ) e. _V )
2 eceldmqs 
 |-  ( ( R |X. ( `' _E |` A ) ) e. _V -> ( [ B ] ( R |X. ( `' _E |` A ) ) e. ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) <-> B e. dom ( R |X. ( `' _E |` A ) ) ) )
3 1 2 syl 
 |-  ( ( A e. V /\ R e. X ) -> ( [ B ] ( R |X. ( `' _E |` A ) ) e. ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) <-> B e. dom ( R |X. ( `' _E |` A ) ) ) )
4 3 3adant2 
 |-  ( ( A e. V /\ B e. W /\ R e. X ) -> ( [ B ] ( R |X. ( `' _E |` A ) ) e. ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) <-> B e. dom ( R |X. ( `' _E |` A ) ) ) )
5 eldmxrncnvepres2 
 |-  ( B e. W -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ E. x x e. B /\ E. y B R y ) ) )
6 5 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ R e. X ) -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ E. x x e. B /\ E. y B R y ) ) )
7 4 6 bitrd 
 |-  ( ( A e. V /\ B e. W /\ R e. X ) -> ( [ B ] ( R |X. ( `' _E |` A ) ) e. ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) <-> ( B e. A /\ E. x x e. B /\ E. y B R y ) ) )