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	⊢ ( ◡ 𝑅 ⊆ 𝑅 → ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅 ) ⊆ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rnss	⊢ ( ◡ 𝑅 ⊆ 𝑅 → ran ◡ 𝑅 ⊆ ran 𝑅 )
2		rncnv	⊢ ran ◡ 𝑅 = dom 𝑅
3	2	sseq1i	⊢ ( ran ◡ 𝑅 ⊆ ran 𝑅 ↔ dom 𝑅 ⊆ ran 𝑅 )
4	3	biimpi	⊢ ( ran ◡ 𝑅 ⊆ ran 𝑅 → dom 𝑅 ⊆ ran 𝑅 )
5		idreseqidinxp	⊢ ( dom 𝑅 ⊆ ran 𝑅 → ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) = ( I ↾ dom 𝑅 ) )
6	1 4 5	3syl	⊢ ( ◡ 𝑅 ⊆ 𝑅 → ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) = ( I ↾ dom 𝑅 ) )
7	6	sseq1d	⊢ ( ◡ 𝑅 ⊆ 𝑅 → ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅 ) ⊆ 𝑅 ) )