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+ A = ( TC+ U. A u. A )

Proof

Step	Hyp	Ref	Expression
1		ssun2	|- A C_ ( TC+ U. A u. A )
2		uniun	|- U. ( TC+ U. A u. A ) = ( U. TC+ U. A u. U. A )
3		ttctr3	|- U. TC+ U. A C_ TC+ U. A
4		ttcid	|- U. A C_ TC+ U. A
5	3 4	unssi	|- ( U. TC+ U. A u. U. A ) C_ TC+ U. A
6	2 5	eqsstri	|- U. ( TC+ U. A u. A ) C_ TC+ U. A
7		ssun3	|- ( U. ( TC+ U. A u. A ) C_ TC+ U. A -> U. ( TC+ U. A u. A ) C_ ( TC+ U. A u. A ) )
8	6 7	ax-mp	|- U. ( TC+ U. A u. A ) C_ ( TC+ U. A u. A )
9		df-tr	|- ( Tr ( TC+ U. A u. A ) <-> U. ( TC+ U. A u. A ) C_ ( TC+ U. A u. A ) )
10	8 9	mpbir	|- Tr ( TC+ U. A u. A )
11		ttcmin	|- ( ( A C_ ( TC+ U. A u. A ) /\ Tr ( TC+ U. A u. A ) ) -> TC+ A C_ ( TC+ U. A u. A ) )
12	1 10 11	mp2an	|- TC+ A C_ ( TC+ U. A u. A )
13		ttcid	|- A C_ TC+ A
14	13	unissi	|- U. A C_ U. TC+ A
15		ttctr3	|- U. TC+ A C_ TC+ A
16	14 15	sstri	|- U. A C_ TC+ A
17		ttcss	|- ( U. A C_ TC+ A -> TC+ U. A C_ TC+ A )
18	16 17	ax-mp	|- TC+ U. A C_ TC+ A
19	18 13	unssi	|- ( TC+ U. A u. A ) C_ TC+ A
20	12 19	eqssi	|- TC+ A = ( TC+ U. A u. A )