Theorem cottrcl

Description: Composition law for the transitive closure of a relation. (Contributed by Scott Fenton, 20-Oct-2024)

	Ref	Expression
Assertion	cottrcl	⊢ ( 𝑅 ∘ t++ 𝑅 ) ⊆ t++ 𝑅

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( 𝑅 ↾ V )
2		ssttrcl	⊢ ( Rel ( 𝑅 ↾ V ) → ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V ) )
3	1 2	ax-mp	⊢ ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V )
4		coss1	⊢ ( ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V ) → ( ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) ⊆ ( t++ ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) )
5	3 4	ax-mp	⊢ ( ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) ⊆ ( t++ ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) )
6		ttrcltr	⊢ ( t++ ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) ⊆ t++ ( 𝑅 ↾ V )
7	5 6	sstri	⊢ ( ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) ⊆ t++ ( 𝑅 ↾ V )
8		ssv	⊢ ran t++ ( 𝑅 ↾ V ) ⊆ V
9		cores	⊢ ( ran t++ ( 𝑅 ↾ V ) ⊆ V → ( ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) = ( 𝑅 ∘ t++ ( 𝑅 ↾ V ) ) )
10	8 9	ax-mp	⊢ ( ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) = ( 𝑅 ∘ t++ ( 𝑅 ↾ V ) )
11		ttrclresv	⊢ t++ ( 𝑅 ↾ V ) = t++ 𝑅
12	11	coeq2i	⊢ ( 𝑅 ∘ t++ ( 𝑅 ↾ V ) ) = ( 𝑅 ∘ t++ 𝑅 )
13	10 12	eqtri	⊢ ( ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) = ( 𝑅 ∘ t++ 𝑅 )
14	7 13 11	3sstr3i	⊢ ( 𝑅 ∘ t++ 𝑅 ) ⊆ t++ 𝑅