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 ) ) )