Metamath Proof Explorer


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 ∩ 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 𝑟 ) ⊆ 𝑟 𝑟𝑟 ) }