elrefsymrels2

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, 22-Jul-2019)

		Ref	Expression
	Assertion	elrefsymrels2	⊢ ( 𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ^◡ 𝑅 ⊆ 𝑅 ) ∧ 𝑅 ∈ Rels ) )

Proof

Step	Hyp	Ref	Expression
1		refsymrels2	⊢ ( RefRels ∩ SymRels ) = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) }
2		dmeq	⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
3	2	reseq2d	⊢ ( 𝑟 = 𝑅 → ( I ↾ dom 𝑟 ) = ( I ↾ dom 𝑅 ) )
4		id	⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
5	3 4	sseq12d	⊢ ( 𝑟 = 𝑅 → ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ↔ ( I ↾ dom 𝑅 ) ⊆ 𝑅 ) )
6		cnveq	⊢ ( 𝑟 = 𝑅 → ^◡ 𝑟 = ^◡ 𝑅 )
7	6 4	sseq12d	⊢ ( 𝑟 = 𝑅 → ( ^◡ 𝑟 ⊆ 𝑟 ↔ ^◡ 𝑅 ⊆ 𝑅 ) )
8	5 7	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) ↔ ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ^◡ 𝑅 ⊆ 𝑅 ) ) )
9	1 8	rabeqel	⊢ ( 𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ^◡ 𝑅 ⊆ 𝑅 ) ∧ 𝑅 ∈ Rels ) )

Metamath Proof Explorer

Theorem elrefsymrels2

Proof