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

Metamath Proof Explorer

Theorem eldmxrncnvepres2

Description: Element of the domain of the range product with restricted converse epsilon relation. This identifies the domain of the pet span ( R |X. (`' _E |`A ) ) : a B belongs to the domain of the span exactly when B is in A and has at least one x e. B and y with B R y . (Contributed by Peter Mazsa, 23-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 eldmres 
 |-  ( B e. V -> ( B e. dom ( R |` A ) <-> ( B e. A /\ E. y B R y ) ) )
2 n0 
 |-  ( B =/= (/) <-> E. x x e. B )
3 2 a1i 
 |-  ( B e. V -> ( B =/= (/) <-> E. x x e. B ) )
4 1 3 anbi12d 
 |-  ( B e. V -> ( ( B e. dom ( R |` A ) /\ B =/= (/) ) <-> ( ( B e. A /\ E. y B R y ) /\ E. x x e. B ) ) )
5 dmxrncnvepres 
 |-  dom ( R |X. ( `' _E |` A ) ) = ( dom ( R |` A ) \ { (/) } )
6 5 eleq2i 
 |-  ( B e. dom ( R |X. ( `' _E |` A ) ) <-> B e. ( dom ( R |` A ) \ { (/) } ) )
7 eldifsn 
 |-  ( B e. ( dom ( R |` A ) \ { (/) } ) <-> ( B e. dom ( R |` A ) /\ B =/= (/) ) )
8 6 7 bitri 
 |-  ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. dom ( R |` A ) /\ B =/= (/) ) )
9 3anan32 
 |-  ( ( B e. A /\ E. x x e. B /\ E. y B R y ) <-> ( ( B e. A /\ E. y B R y ) /\ E. x x e. B ) )
10 4 8 9 3bitr4g 
 |-  ( B e. V -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ E. x x e. B /\ E. y B R y ) ) )