This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrefrels2

Description: Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019)

Ref Expression
Assertion elrefrels2 ( 𝑅 ∈ RefRels ↔ ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ) )

Proof

Step Hyp Ref Expression
1 dfrefrels2 ⊢ RefRels = { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 }
2 dmeq ⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
3 rneq ⊢ ( 𝑟 = 𝑅 → ran 𝑟 = ran 𝑅 )
4 2 3 xpeq12d ⊢ ( 𝑟 = 𝑅 → ( dom 𝑟 × ran 𝑟 ) = ( dom 𝑅 × ran 𝑅 ) )
5 4 ineq2d ⊢ ( 𝑟 = 𝑅 → ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) = ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) )
6 id ⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
7 5 6 sseq12d ⊢ ( 𝑟 = 𝑅 → ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ↔ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ) )
8 1 7 rabeqel ⊢ ( 𝑅 ∈ RefRels ↔ ( ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ) )