Metamath Proof Explorer

Theorem dfeqvrels2

Description: Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019)

Ref Expression
Assertion dfeqvrels2 
|- EqvRels = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r /\ ( r o. r ) C_ r ) }

Proof

Step Hyp Ref Expression
1 df-eqvrels 
 |-  EqvRels = ( ( RefRels i^i SymRels ) i^i TrRels )
2 refsymrels2 
 |-  ( RefRels i^i SymRels ) = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) }
3 dftrrels2 
 |-  TrRels = { r e. Rels | ( r o. r ) C_ r }
4 2 3 ineq12i 
 |-  ( ( RefRels i^i SymRels ) i^i TrRels ) = ( { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) } i^i { r e. Rels | ( r o. r ) C_ r } )
5 inrab 
 |-  ( { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) } i^i { r e. Rels | ( r o. r ) C_ r } ) = { r e. Rels | ( ( ( _I |` dom r ) C_ r /\ `' r C_ r ) /\ ( r o. r ) C_ r ) }
6 1 4 5 3eqtri 
 |-  EqvRels = { r e. Rels | ( ( ( _I |` dom r ) C_ r /\ `' r C_ r ) /\ ( r o. r ) C_ r ) }
7 df-3an 
 |-  ( ( ( _I |` dom r ) C_ r /\ `' r C_ r /\ ( r o. r ) C_ r ) <-> ( ( ( _I |` dom r ) C_ r /\ `' r C_ r ) /\ ( r o. r ) C_ r ) )
8 7 rabbii 
 |-  { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r /\ ( r o. r ) C_ r ) } = { r e. Rels | ( ( ( _I |` dom r ) C_ r /\ `' r C_ r ) /\ ( r o. r ) C_ r ) }
9 6 8 eqtr4i 
 |-  EqvRels = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r /\ ( r o. r ) C_ r ) }