Theorem symrefref2

Description: Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 . (Contributed by Peter Mazsa, 19-Jul-2018)

	Ref	Expression
Assertion	symrefref2	|- ( `' R C_ R -> ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> ( _I |` dom R ) C_ R ) )

Proof

Step	Hyp	Ref	Expression
1		rnss	|- ( `' R C_ R -> ran `' R C_ ran R )
2		rncnv	|- ran `' R = dom R
3	2	sseq1i	|- ( ran `' R C_ ran R <-> dom R C_ ran R )
4	3	biimpi	|- ( ran `' R C_ ran R -> dom R C_ ran R )
5		idreseqidinxp	|- ( dom R C_ ran R -> ( _I i^i ( dom R X. ran R ) ) = ( _I |` dom R ) )
6	1 4 5	3syl	|- ( `' R C_ R -> ( _I i^i ( dom R X. ran R ) ) = ( _I |` dom R ) )
7	6	sseq1d	|- ( `' R C_ R -> ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> ( _I |` dom R ) C_ R ) )