Theorem ttrclco

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

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

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( 𝑅 ↾ V )
2		ssttrcl	⊢ ( Rel ( 𝑅 ↾ V ) → ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V ) )
3		coss2	⊢ ( ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V ) → ( t++ ( 𝑅 ↾ V ) ∘ ( 𝑅 ↾ V ) ) ⊆ ( t++ ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) )
4	1 2 3	mp2b	⊢ ( t++ ( 𝑅 ↾ V ) ∘ ( 𝑅 ↾ V ) ) ⊆ ( t++ ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) )
5		ttrcltr	⊢ ( t++ ( 𝑅 ↾ V ) ∘ t++ ( 𝑅 ↾ V ) ) ⊆ t++ ( 𝑅 ↾ V )
6	4 5	sstri	⊢ ( t++ ( 𝑅 ↾ V ) ∘ ( 𝑅 ↾ V ) ) ⊆ t++ ( 𝑅 ↾ V )
7		relco	⊢ Rel ( t++ ( 𝑅 ↾ V ) ∘ 𝑅 )
8		dfrel3	⊢ ( Rel ( t++ ( 𝑅 ↾ V ) ∘ 𝑅 ) ↔ ( ( t++ ( 𝑅 ↾ V ) ∘ 𝑅 ) ↾ V ) = ( t++ ( 𝑅 ↾ V ) ∘ 𝑅 ) )
9	7 8	mpbi	⊢ ( ( t++ ( 𝑅 ↾ V ) ∘ 𝑅 ) ↾ V ) = ( t++ ( 𝑅 ↾ V ) ∘ 𝑅 )
10		resco	⊢ ( ( t++ ( 𝑅 ↾ V ) ∘ 𝑅 ) ↾ V ) = ( t++ ( 𝑅 ↾ V ) ∘ ( 𝑅 ↾ V ) )
11		ttrclresv	⊢ t++ ( 𝑅 ↾ V ) = t++ 𝑅
12	11	coeq1i	⊢ ( t++ ( 𝑅 ↾ V ) ∘ 𝑅 ) = ( t++ 𝑅 ∘ 𝑅 )
13	9 10 12	3eqtr3i	⊢ ( t++ ( 𝑅 ↾ V ) ∘ ( 𝑅 ↾ V ) ) = ( t++ 𝑅 ∘ 𝑅 )
14	6 13 11	3sstr3i	⊢ ( t++ 𝑅 ∘ 𝑅 ) ⊆ t++ 𝑅