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 ) }