Theorem ttrclco

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

	Ref	Expression
Assertion	ttrclco	Could not format assertion : No typesetting found for |- ( t++ R o. 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		coss2	Could not format ( ( R |` _V ) C_ t++ ( R |` _V ) -> ( t++ ( R |` _V ) o. ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) ) : No typesetting found for |- ( ( R |` _V ) C_ t++ ( R |` _V ) -> ( t++ ( R |` _V ) o. ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) ) with typecode |-
4	1 2 3	mp2b	Could not format ( t++ ( R |` _V ) o. ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) : No typesetting found for |- ( t++ ( R |` _V ) o. ( R |` _V ) ) C_ ( t++ ( R |` _V ) o. t++ ( R |` _V ) ) with typecode |-
5		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 |-
6	4 5	sstri	Could not format ( t++ ( R |` _V ) o. ( R |` _V ) ) C_ t++ ( R |` _V ) : No typesetting found for |- ( t++ ( R |` _V ) o. ( R |` _V ) ) C_ t++ ( R |` _V ) with typecode |-
7		relco	Could not format Rel ( t++ ( R |` _V ) o. R ) : No typesetting found for |- Rel ( t++ ( R |` _V ) o. R ) with typecode |-
8		dfrel3	Could not format ( Rel ( t++ ( R |` _V ) o. R ) <-> ( ( t++ ( R |` _V ) o. R ) |` _V ) = ( t++ ( R |` _V ) o. R ) ) : No typesetting found for |- ( Rel ( t++ ( R |` _V ) o. R ) <-> ( ( t++ ( R |` _V ) o. R ) |` _V ) = ( t++ ( R |` _V ) o. R ) ) with typecode |-
9	7 8	mpbi	Could not format ( ( t++ ( R |` _V ) o. R ) |` _V ) = ( t++ ( R |` _V ) o. R ) : No typesetting found for |- ( ( t++ ( R |` _V ) o. R ) |` _V ) = ( t++ ( R |` _V ) o. R ) with typecode |-
10		resco	Could not format ( ( t++ ( R |` _V ) o. R ) |` _V ) = ( t++ ( R |` _V ) o. ( R |` _V ) ) : No typesetting found for |- ( ( t++ ( R |` _V ) o. R ) |` _V ) = ( t++ ( R |` _V ) o. ( 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	coeq1i	Could not format ( t++ ( R |` _V ) o. R ) = ( t++ R o. R ) : No typesetting found for |- ( t++ ( R |` _V ) o. R ) = ( t++ R o. R ) with typecode |-
13	9 10 12	3eqtr3i	Could not format ( t++ ( R |` _V ) o. ( R |` _V ) ) = ( t++ R o. R ) : No typesetting found for |- ( t++ ( R |` _V ) o. ( R |` _V ) ) = ( t++ R o. R ) with typecode |-
14	6 13 11	3sstr3i	Could not format ( t++ R o. R ) C_ t++ R : No typesetting found for |- ( t++ R o. R ) C_ t++ R with typecode |-