Metamath Proof Explorer


Theorem eltrrels2

Description: Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021)

Ref Expression
Assertion eltrrels2 ( 𝑅 ∈ TrRels ↔ ( ( 𝑅𝑅 ) ⊆ 𝑅𝑅 ∈ Rels ) )

Proof

Step Hyp Ref Expression
1 dftrrels2 TrRels = { 𝑟 ∈ Rels ∣ ( 𝑟𝑟 ) ⊆ 𝑟 }
2 coideq ( 𝑟 = 𝑅 → ( 𝑟𝑟 ) = ( 𝑅𝑅 ) )
3 id ( 𝑟 = 𝑅𝑟 = 𝑅 )
4 2 3 sseq12d ( 𝑟 = 𝑅 → ( ( 𝑟𝑟 ) ⊆ 𝑟 ↔ ( 𝑅𝑅 ) ⊆ 𝑅 ) )
5 1 4 rabeqel ( 𝑅 ∈ TrRels ↔ ( ( 𝑅𝑅 ) ⊆ 𝑅𝑅 ∈ Rels ) )