Metamath Proof Explorer


Theorem reltrclfv

Description: The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020)

Ref Expression
Assertion reltrclfv ( ( 𝑅𝑉 ∧ Rel 𝑅 ) → Rel ( t+ ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 trclfvub ( 𝑅𝑉 → ( t+ ‘ 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
2 1 adantr ( ( 𝑅𝑉 ∧ Rel 𝑅 ) → ( t+ ‘ 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
3 simpr ( ( 𝑅𝑉 ∧ Rel 𝑅 ) → Rel 𝑅 )
4 relssdmrn ( Rel 𝑅𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
5 ssequn1 ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ↔ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) )
6 5 biimpi ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) )
7 3 4 6 3syl ( ( 𝑅𝑉 ∧ Rel 𝑅 ) → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) )
8 2 7 sseqtrd ( ( 𝑅𝑉 ∧ Rel 𝑅 ) → ( t+ ‘ 𝑅 ) ⊆ ( dom 𝑅 × ran 𝑅 ) )
9 xpss ( dom 𝑅 × ran 𝑅 ) ⊆ ( V × V )
10 8 9 sstrdi ( ( 𝑅𝑉 ∧ Rel 𝑅 ) → ( t+ ‘ 𝑅 ) ⊆ ( V × V ) )
11 df-rel ( Rel ( t+ ‘ 𝑅 ) ↔ ( t+ ‘ 𝑅 ) ⊆ ( V × V ) )
12 10 11 sylibr ( ( 𝑅𝑉 ∧ Rel 𝑅 ) → Rel ( t+ ‘ 𝑅 ) )