This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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