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

Metamath Proof Explorer

Theorem eqvrelcoss3

Description: Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019)

Ref Expression
Assertion eqvrelcoss3 
|- ( EqvRel ,~ R <-> A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) )

Proof

Step Hyp Ref Expression
1 relcoss 
 |-  Rel ,~ R
2 1 biantru 
 |-  ( ( A. x e. dom ,~ R x ,~ R x /\ A. x A. y ( x ,~ R y -> y ,~ R x ) /\ A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) ) <-> ( ( A. x e. dom ,~ R x ,~ R x /\ A. x A. y ( x ,~ R y -> y ,~ R x ) /\ A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) ) /\ Rel ,~ R ) )
3 refrelcosslem 
 |-  A. x e. dom ,~ R x ,~ R x
4 symrelcoss3 
 |-  ( A. x A. y ( x ,~ R y -> y ,~ R x ) /\ Rel ,~ R )
5 4 simpli 
 |-  A. x A. y ( x ,~ R y -> y ,~ R x )
6 3 5 triantru3 
 |-  ( A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) <-> ( A. x e. dom ,~ R x ,~ R x /\ A. x A. y ( x ,~ R y -> y ,~ R x ) /\ A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) ) )
7 dfeqvrel3 
 |-  ( EqvRel ,~ R <-> ( ( A. x e. dom ,~ R x ,~ R x /\ A. x A. y ( x ,~ R y -> y ,~ R x ) /\ A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) ) /\ Rel ,~ R ) )
8 2 6 7 3bitr4ri 
 |-  ( EqvRel ,~ R <-> A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) )