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

Metamath Proof Explorer

Theorem eceldmqsxrncnvepres

Description: An ( R |X. (`' _E |`A ) ) -coset in its domain quotient. (Contributed by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion eceldmqsxrncnvepres 
|- ( ( 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 /\ B =/= (/) /\ [ B ] R =/= (/) ) ) )

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 eldmxrncnvepres 
 |-  ( B e. W -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ B =/= (/) /\ [ B ] R =/= (/) ) ) )
6 5 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ R e. X ) -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ B =/= (/) /\ [ B ] R =/= (/) ) ) )
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 /\ B =/= (/) /\ [ B ] R =/= (/) ) ) )