Metamath Proof Explorer

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 
|- ( A e. TC+ B -> TC+ A C_ TC+ B )

Proof

Step Hyp Ref Expression
1 ttctr2 
 |-  ( A e. TC+ B -> A C_ TC+ B )
2 ttctr 
 |-  Tr TC+ B
3 ttcmin 
 |-  ( ( A C_ TC+ B /\ Tr TC+ B ) -> TC+ A C_ TC+ B )
4 1 2 3 sylancl 
 |-  ( A e. TC+ B -> TC+ A C_ TC+ B )