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

Metamath Proof Explorer

Theorem refsymrels2

Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels2 ) can use the restricted version for their reflexive part (see below), not just the (I i^i ( dom r X. ran r ) ) C r version of dfrefrels2 , cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 20-Jul-2019)

Ref Expression
Assertion refsymrels2 
|- ( RefRels i^i SymRels ) = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) }

Proof

Step Hyp Ref Expression
1 dfrefrels2 
 |-  RefRels = { r e. Rels | ( _I i^i ( dom r X. ran r ) ) C_ r }
2 dfsymrels2 
 |-  SymRels = { r e. Rels | `' r C_ r }
3 1 2 ineq12i 
 |-  ( RefRels i^i SymRels ) = ( { r e. Rels | ( _I i^i ( dom r X. ran r ) ) C_ r } i^i { r e. Rels | `' r C_ r } )
4 inrab 
 |-  ( { r e. Rels | ( _I i^i ( dom r X. ran r ) ) C_ r } i^i { r e. Rels | `' r C_ r } ) = { r e. Rels | ( ( _I i^i ( dom r X. ran r ) ) C_ r /\ `' r C_ r ) }
5 symrefref2 
 |-  ( `' r C_ r -> ( ( _I i^i ( dom r X. ran r ) ) C_ r <-> ( _I |` dom r ) C_ r ) )
6 5 pm5.32ri 
 |-  ( ( ( _I i^i ( dom r X. ran r ) ) C_ r /\ `' r C_ r ) <-> ( ( _I |` dom r ) C_ r /\ `' r C_ r ) )
7 6 rabbii 
 |-  { r e. Rels | ( ( _I i^i ( dom r X. ran r ) ) C_ r /\ `' r C_ r ) } = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) }
8 3 4 7 3eqtri 
 |-  ( RefRels i^i SymRels ) = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) }