Theorem ttcuni

Description: Distribute union of a class through a transitive closure. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcuni	|- TC+ U. A = U. TC+ A

Proof

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