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 ∩ SymRels ) = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) }

Proof

Step	Hyp	Ref	Expression
1		dfrefrels2	⊢ RefRels = { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 }
2		dfsymrels2	⊢ SymRels = { 𝑟 ∈ Rels ∣ ^◡ 𝑟 ⊆ 𝑟 }
3	1 2	ineq12i	⊢ ( RefRels ∩ SymRels ) = ( { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 } ∩ { 𝑟 ∈ Rels ∣ ^◡ 𝑟 ⊆ 𝑟 } )
4		inrab	⊢ ( { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 } ∩ { 𝑟 ∈ Rels ∣ ^◡ 𝑟 ⊆ 𝑟 } ) = { 𝑟 ∈ Rels ∣ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) }
5		symrefref2	⊢ ( ^◡ 𝑟 ⊆ 𝑟 → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ↔ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ) )
6	5	pm5.32ri	⊢ ( ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) ↔ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) )
7	6	rabbii	⊢ { 𝑟 ∈ Rels ∣ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) } = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) }
8	3 4 7	3eqtri	⊢ ( RefRels ∩ SymRels ) = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ^◡ 𝑟 ⊆ 𝑟 ) }

Metamath Proof Explorer

Theorem refsymrels2

Proof