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+ ‘ 𝑅 ) )