Theorem ttcuni

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

	Ref	Expression
Assertion	ttcuni	⊢ TC+ ∪ 𝐴 = ∪ TC+ 𝐴

Proof

Step	Hyp	Ref	Expression
1		ttcid	⊢ 𝐴 ⊆ TC+ 𝐴
2	1	unissi	⊢ ∪ 𝐴 ⊆ ∪ TC+ 𝐴
3		ttctr3	⊢ ∪ TC+ 𝐴 ⊆ TC+ 𝐴
4	3	unissi	⊢ ∪ ∪ TC+ 𝐴 ⊆ ∪ TC+ 𝐴
5		df-tr	⊢ ( Tr ∪ TC+ 𝐴 ↔ ∪ ∪ TC+ 𝐴 ⊆ ∪ TC+ 𝐴 )
6	4 5	mpbir	⊢ Tr ∪ TC+ 𝐴
7		ttcmin	⊢ ( ( ∪ 𝐴 ⊆ ∪ TC+ 𝐴 ∧ Tr ∪ TC+ 𝐴 ) → TC+ ∪ 𝐴 ⊆ ∪ TC+ 𝐴 )
8	2 6 7	mp2an	⊢ TC+ ∪ 𝐴 ⊆ ∪ TC+ 𝐴
9		ttcuniun	⊢ TC+ 𝐴 = ( TC+ ∪ 𝐴 ∪ 𝐴 )
10	9	unieqi	⊢ ∪ TC+ 𝐴 = ∪ ( TC+ ∪ 𝐴 ∪ 𝐴 )
11		uniun	⊢ ∪ ( TC+ ∪ 𝐴 ∪ 𝐴 ) = ( ∪ TC+ ∪ 𝐴 ∪ ∪ 𝐴 )
12	10 11	eqtri	⊢ ∪ TC+ 𝐴 = ( ∪ TC+ ∪ 𝐴 ∪ ∪ 𝐴 )
13		ttctr3	⊢ ∪ TC+ ∪ 𝐴 ⊆ TC+ ∪ 𝐴
14		ttcid	⊢ ∪ 𝐴 ⊆ TC+ ∪ 𝐴
15	13 14	unssi	⊢ ( ∪ TC+ ∪ 𝐴 ∪ ∪ 𝐴 ) ⊆ TC+ ∪ 𝐴
16	12 15	eqsstri	⊢ ∪ TC+ 𝐴 ⊆ TC+ ∪ 𝐴
17	8 16	eqssi	⊢ TC+ ∪ 𝐴 = ∪ TC+ 𝐴