Theorem ttciun

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

	Ref	Expression
Assertion	ttciun	⊢ TC+ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 TC+ 𝐵

Proof

Step	Hyp	Ref	Expression
1		iunxiun	⊢ ∪ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 TC+ 𝑦 = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 TC+ 𝑦
2	1	uneq1i	⊢ ( ∪ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 TC+ 𝑦 ∪ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 TC+ 𝑦 ∪ ∪ 𝑥 ∈ 𝐴 𝐵 )
3		iunun	⊢ ∪ 𝑥 ∈ 𝐴 ( ∪ 𝑦 ∈ 𝐵 TC+ 𝑦 ∪ 𝐵 ) = ( ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 TC+ 𝑦 ∪ ∪ 𝑥 ∈ 𝐴 𝐵 )
4	2 3	eqtr4i	⊢ ( ∪ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 TC+ 𝑦 ∪ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( ∪ 𝑦 ∈ 𝐵 TC+ 𝑦 ∪ 𝐵 )
5		ttciunun	⊢ TC+ ∪ 𝑥 ∈ 𝐴 𝐵 = ( ∪ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 TC+ 𝑦 ∪ ∪ 𝑥 ∈ 𝐴 𝐵 )
6		ttciunun	⊢ TC+ 𝐵 = ( ∪ 𝑦 ∈ 𝐵 TC+ 𝑦 ∪ 𝐵 )
7	6	a1i	⊢ ( 𝑥 ∈ 𝐴 → TC+ 𝐵 = ( ∪ 𝑦 ∈ 𝐵 TC+ 𝑦 ∪ 𝐵 ) )
8	7	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 TC+ 𝐵 = ∪ 𝑥 ∈ 𝐴 ( ∪ 𝑦 ∈ 𝐵 TC+ 𝑦 ∪ 𝐵 )
9	4 5 8	3eqtr4i	⊢ TC+ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 TC+ 𝐵