Theorem ttciun

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

	Ref	Expression
Assertion	ttciun	|- TC+ U_ x e. A B = U_ x e. A TC+ B

Proof

Step	Hyp	Ref	Expression
1		iunxiun	|- U_ y e. U_ x e. A B TC+ y = U_ x e. A U_ y e. B TC+ y
2	1	uneq1i	|- ( U_ y e. U_ x e. A B TC+ y u. U_ x e. A B ) = ( U_ x e. A U_ y e. B TC+ y u. U_ x e. A B )
3		iunun	|- U_ x e. A ( U_ y e. B TC+ y u. B ) = ( U_ x e. A U_ y e. B TC+ y u. U_ x e. A B )
4	2 3	eqtr4i	|- ( U_ y e. U_ x e. A B TC+ y u. U_ x e. A B ) = U_ x e. A ( U_ y e. B TC+ y u. B )
5		ttciunun	|- TC+ U_ x e. A B = ( U_ y e. U_ x e. A B TC+ y u. U_ x e. A B )
6		ttciunun	|- TC+ B = ( U_ y e. B TC+ y u. B )
7	6	a1i	|- ( x e. A -> TC+ B = ( U_ y e. B TC+ y u. B ) )
8	7	iuneq2i	|- U_ x e. A TC+ B = U_ x e. A ( U_ y e. B TC+ y u. B )
9	4 5 8	3eqtr4i	|- TC+ U_ x e. A B = U_ x e. A TC+ B