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

Metamath Proof Explorer

Theorem refrelcoss3

Description: The class of cosets by R is reflexive, see dfrefrel3 . (Contributed by Peter Mazsa, 30-Jul-2019)

Ref Expression
Assertion refrelcoss3 
|- ( A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y ) /\ Rel ,~ R )

Proof

Step Hyp Ref Expression
1 refrelcosslem 
 |-  A. x e. dom ,~ R x ,~ R x
2 idinxpssinxp4 
 |-  ( A. x e. dom ,~ R A. y e. dom ,~ R ( x = y -> x ,~ R y ) <-> A. x e. dom ,~ R x ,~ R x )
3 1 2 mpbir 
 |-  A. x e. dom ,~ R A. y e. dom ,~ R ( x = y -> x ,~ R y )
4 rncossdmcoss 
 |-  ran ,~ R = dom ,~ R
5 4 raleqi 
 |-  ( A. y e. ran ,~ R ( x = y -> x ,~ R y ) <-> A. y e. dom ,~ R ( x = y -> x ,~ R y ) )
6 5 ralbii 
 |-  ( A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y ) <-> A. x e. dom ,~ R A. y e. dom ,~ R ( x = y -> x ,~ R y ) )
7 3 6 mpbir 
 |-  A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y )
8 relcoss 
 |-  Rel ,~ R
9 7 8 pm3.2i 
 |-  ( A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y ) /\ Rel ,~ R )