Theorem ttcss2

Description: The subclass relationship is inherited by transitive closures. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcss2	⊢ ( 𝐴 ⊆ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ttcid	⊢ 𝐵 ⊆ TC+ 𝐵
2		sstr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ TC+ 𝐵 ) → 𝐴 ⊆ TC+ 𝐵 )
3	1 2	mpan2	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ TC+ 𝐵 )
4		ttcss	⊢ ( 𝐴 ⊆ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵 )
5	3 4	syl	⊢ ( 𝐴 ⊆ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵 )