Theorem ttcun

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

	Ref	Expression
Assertion	ttcun	⊢ TC+ ( 𝐴 ∪ 𝐵 ) = ( TC+ 𝐴 ∪ TC+ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		un4	⊢ ( ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ ∪ 𝑥 ∈ 𝐵 TC+ 𝑥 ) ∪ ( 𝐴 ∪ 𝐵 ) ) = ( ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) ∪ ( ∪ 𝑥 ∈ 𝐵 TC+ 𝑥 ∪ 𝐵 ) )
2		ttciunun	⊢ TC+ ( 𝐴 ∪ 𝐵 ) = ( ∪ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) TC+ 𝑥 ∪ ( 𝐴 ∪ 𝐵 ) )
3		iunxun	⊢ ∪ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) TC+ 𝑥 = ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ ∪ 𝑥 ∈ 𝐵 TC+ 𝑥 )
4	3	uneq1i	⊢ ( ∪ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) TC+ 𝑥 ∪ ( 𝐴 ∪ 𝐵 ) ) = ( ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ ∪ 𝑥 ∈ 𝐵 TC+ 𝑥 ) ∪ ( 𝐴 ∪ 𝐵 ) )
5	2 4	eqtri	⊢ TC+ ( 𝐴 ∪ 𝐵 ) = ( ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ ∪ 𝑥 ∈ 𝐵 TC+ 𝑥 ) ∪ ( 𝐴 ∪ 𝐵 ) )
6		ttciunun	⊢ TC+ 𝐴 = ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 )
7		ttciunun	⊢ TC+ 𝐵 = ( ∪ 𝑥 ∈ 𝐵 TC+ 𝑥 ∪ 𝐵 )
8	6 7	uneq12i	⊢ ( TC+ 𝐴 ∪ TC+ 𝐵 ) = ( ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) ∪ ( ∪ 𝑥 ∈ 𝐵 TC+ 𝑥 ∪ 𝐵 ) )
9	1 5 8	3eqtr4i	⊢ TC+ ( 𝐴 ∪ 𝐵 ) = ( TC+ 𝐴 ∪ TC+ 𝐵 )