Theorem ttcuniun

Description: Relationship between TC+ A and TC+ U. A : we can decompose TC+ A into the elements of TC+ U. A plus the elements of A itself. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcuniun	⊢ TC+ 𝐴 = ( TC+ ∪ 𝐴 ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssun2	⊢ 𝐴 ⊆ ( TC+ ∪ 𝐴 ∪ 𝐴 )
2		uniun	⊢ ∪ ( TC+ ∪ 𝐴 ∪ 𝐴 ) = ( ∪ TC+ ∪ 𝐴 ∪ ∪ 𝐴 )
3		ttctr3	⊢ ∪ TC+ ∪ 𝐴 ⊆ TC+ ∪ 𝐴
4		ttcid	⊢ ∪ 𝐴 ⊆ TC+ ∪ 𝐴
5	3 4	unssi	⊢ ( ∪ TC+ ∪ 𝐴 ∪ ∪ 𝐴 ) ⊆ TC+ ∪ 𝐴
6	2 5	eqsstri	⊢ ∪ ( TC+ ∪ 𝐴 ∪ 𝐴 ) ⊆ TC+ ∪ 𝐴
7		ssun3	⊢ ( ∪ ( TC+ ∪ 𝐴 ∪ 𝐴 ) ⊆ TC+ ∪ 𝐴 → ∪ ( TC+ ∪ 𝐴 ∪ 𝐴 ) ⊆ ( TC+ ∪ 𝐴 ∪ 𝐴 ) )
8	6 7	ax-mp	⊢ ∪ ( TC+ ∪ 𝐴 ∪ 𝐴 ) ⊆ ( TC+ ∪ 𝐴 ∪ 𝐴 )
9		df-tr	⊢ ( Tr ( TC+ ∪ 𝐴 ∪ 𝐴 ) ↔ ∪ ( TC+ ∪ 𝐴 ∪ 𝐴 ) ⊆ ( TC+ ∪ 𝐴 ∪ 𝐴 ) )
10	8 9	mpbir	⊢ Tr ( TC+ ∪ 𝐴 ∪ 𝐴 )
11		ttcmin	⊢ ( ( 𝐴 ⊆ ( TC+ ∪ 𝐴 ∪ 𝐴 ) ∧ Tr ( TC+ ∪ 𝐴 ∪ 𝐴 ) ) → TC+ 𝐴 ⊆ ( TC+ ∪ 𝐴 ∪ 𝐴 ) )
12	1 10 11	mp2an	⊢ TC+ 𝐴 ⊆ ( TC+ ∪ 𝐴 ∪ 𝐴 )
13		ttcid	⊢ 𝐴 ⊆ TC+ 𝐴
14	13	unissi	⊢ ∪ 𝐴 ⊆ ∪ TC+ 𝐴
15		ttctr3	⊢ ∪ TC+ 𝐴 ⊆ TC+ 𝐴
16	14 15	sstri	⊢ ∪ 𝐴 ⊆ TC+ 𝐴
17		ttcss	⊢ ( ∪ 𝐴 ⊆ TC+ 𝐴 → TC+ ∪ 𝐴 ⊆ TC+ 𝐴 )
18	16 17	ax-mp	⊢ TC+ ∪ 𝐴 ⊆ TC+ 𝐴
19	18 13	unssi	⊢ ( TC+ ∪ 𝐴 ∪ 𝐴 ) ⊆ TC+ 𝐴
20	12 19	eqssi	⊢ TC+ 𝐴 = ( TC+ ∪ 𝐴 ∪ 𝐴 )