Theorem cottrcl

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

	Ref	Expression
Assertion	cottrcl	Could not format assertion : No typesetting found for |- ( R o. t++ R ) C_ t++ R with typecode |-

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({R\upharpoonright }_{\mathrm{V}}\right)$$
2		ssttrcl	Could not format ( Rel ( R |` _V ) -> ( R |` _V ) C_ t++ ( R |` _V ) ) : No typesetting found for |- ( Rel ( R |` _V ) -> ( R |` _V ) C_ t++ ( R |` _V ) ) with typecode |-
3	1 2	ax-mp	Could not format ( R |` _V ) C_ t++ ( R |` _V ) : No typesetting found for |- ( R |` _V ) C_ t++ ( R |` _V ) with typecode |-
4		coss1	Could not format ( ( R |` _V ) C_ t++ ( R |` _V ) -> ( ( R |` _V ) o. t++ ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) ) : No typesetting found for |- ( ( R |` _V ) C_ t++ ( R |` _V ) -> ( ( R |` _V ) o. t++ ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) ) with typecode |-
5	3 4	ax-mp	Could not format ( ( R |` _V ) o. t++ ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) : No typesetting found for |- ( ( R |` _V ) o. t++ ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) with typecode |-
6		ttrcltr	Could not format ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) C_ t++ ( R |` _V ) : No typesetting found for |- ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) C_ t++ ( R |` _V ) with typecode |-
7	5 6	sstri	Could not format ( ( R |` _V ) o. t++ ( R |` _V ) ) C_ t++ ( R |` _V ) : No typesetting found for |- ( ( R |` _V ) o. t++ ( R |` _V ) ) C_ t++ ( R |` _V ) with typecode |-
8		ssv	Could not format ran t++ ( R |` _V ) C_ _V : No typesetting found for |- ran t++ ( R |` _V ) C_ _V with typecode |-
9		cores	Could not format ( ran t++ ( R |` _V ) C_ _V -> ( ( R |` _V ) o. t++ ( R |` _V ) ) = ( R o. t++ ( R |` _V ) ) ) : No typesetting found for |- ( ran t++ ( R |` _V ) C_ _V -> ( ( R |` _V ) o. t++ ( R |` _V ) ) = ( R o. t++ ( R |` _V ) ) ) with typecode |-
10	8 9	ax-mp	Could not format ( ( R |` _V ) o. t++ ( R |` _V ) ) = ( R o. t++ ( R |` _V ) ) : No typesetting found for |- ( ( R |` _V ) o. t++ ( R |` _V ) ) = ( R o. t++ ( R |` _V ) ) with typecode |-
11		ttrclresv	Could not format t++ ( R |` _V ) = t++ R : No typesetting found for |- t++ ( R |` _V ) = t++ R with typecode |-
12	11	coeq2i	Could not format ( R o. t++ ( R |` _V ) ) = ( R o. t++ R ) : No typesetting found for |- ( R o. t++ ( R |` _V ) ) = ( R o. t++ R ) with typecode |-
13	10 12	eqtri	Could not format ( ( R |` _V ) o. t++ ( R |` _V ) ) = ( R o. t++ R ) : No typesetting found for |- ( ( R |` _V ) o. t++ ( R |` _V ) ) = ( R o. t++ R ) with typecode |-
14	7 13 11	3sstr3i	Could not format ( R o. t++ R ) C_ t++ R : No typesetting found for |- ( R o. t++ R ) C_ t++ R with typecode |-