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

Metamath Proof Explorer

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