Theorem ttcel

Description: A transitive closure contains the transitive closures of all its elements. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcel	Could not format assertion : No typesetting found for |- ( A e. TC+ B -> TC+ A C_ TC+ B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ttctr2	Could not format ( A e. TC+ B -> A C_ TC+ B ) : No typesetting found for |- ( A e. TC+ B -> A C_ TC+ B ) with typecode |-
2		ttctr	Could not format Tr TC+ B : No typesetting found for |- Tr TC+ B with typecode |-
3		ttcmin	Could not format ( ( A C_ TC+ B /\ Tr TC+ B ) -> TC+ A C_ TC+ B ) : No typesetting found for |- ( ( A C_ TC+ B /\ Tr TC+ B ) -> TC+ A C_ TC+ B ) with typecode |-
4	1 2 3	sylancl	Could not format ( A e. TC+ B -> TC+ A C_ TC+ B ) : No typesetting found for |- ( A e. TC+ B -> TC+ A C_ TC+ B ) with typecode |-