Theorem ttciunun

Description: Relationship between TC+ A and U_ x e. A TC+ x : we can decompose TC+ A into the elements of U_ x e. A TC+ x plus the elements of A itself. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttciunun	⊢ TC+ 𝐴 = ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssun2	⊢ 𝐴 ⊆ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 )
2		dftr3	⊢ ( Tr ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) ↔ ∀ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) 𝑦 ⊆ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) )
3		elun	⊢ ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) ↔ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∨ 𝑦 ∈ 𝐴 ) )
4		ttctr	⊢ Tr TC+ 𝑥
5	4	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 Tr TC+ 𝑥
6		triun	⊢ ( ∀ 𝑥 ∈ 𝐴 Tr TC+ 𝑥 → Tr ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 )
7		trss	⊢ ( Tr ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 → ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ) )
8	5 6 7	mp2b	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 )
9		ttcid	⊢ 𝑦 ⊆ TC+ 𝑦
10		ttceq	⊢ ( 𝑥 = 𝑦 → TC+ 𝑥 = TC+ 𝑦 )
11	10	ssiun2s	⊢ ( 𝑦 ∈ 𝐴 → TC+ 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 )
12	9 11	sstrid	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 )
13	8 12	jaoi	⊢ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∨ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 )
14	3 13	sylbi	⊢ ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 )
15		ssun3	⊢ ( 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 → 𝑦 ⊆ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) )
16	14 15	syl	⊢ ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) → 𝑦 ⊆ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) )
17	2 16	mprgbir	⊢ Tr ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 )
18		ttcmin	⊢ ( ( 𝐴 ⊆ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) ∧ Tr ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) ) → TC+ 𝐴 ⊆ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) )
19	1 17 18	mp2an	⊢ TC+ 𝐴 ⊆ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 )
20		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ⊆ TC+ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 TC+ 𝑥 ⊆ TC+ 𝐴 )
21		ttcel2	⊢ ( 𝑥 ∈ 𝐴 → TC+ 𝑥 ⊆ TC+ 𝐴 )
22	20 21	mprgbir	⊢ ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ⊆ TC+ 𝐴
23		ttcid	⊢ 𝐴 ⊆ TC+ 𝐴
24	22 23	unssi	⊢ ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 ) ⊆ TC+ 𝐴
25	19 24	eqssi	⊢ TC+ 𝐴 = ( ∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴 )