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+ A = ( U_ x e. A TC+ x u. A )

Proof

Step	Hyp	Ref	Expression
1		ssun2	|- A C_ ( U_ x e. A TC+ x u. A )
2		dftr3	|- ( Tr ( U_ x e. A TC+ x u. A ) <-> A. y e. ( U_ x e. A TC+ x u. A ) y C_ ( U_ x e. A TC+ x u. A ) )
3		elun	|- ( y e. ( U_ x e. A TC+ x u. A ) <-> ( y e. U_ x e. A TC+ x \/ y e. A ) )
4		ttctr	|- Tr TC+ x
5	4	rgenw	|- A. x e. A Tr TC+ x
6		triun	|- ( A. x e. A Tr TC+ x -> Tr U_ x e. A TC+ x )
7		trss	|- ( Tr U_ x e. A TC+ x -> ( y e. U_ x e. A TC+ x -> y C_ U_ x e. A TC+ x ) )
8	5 6 7	mp2b	|- ( y e. U_ x e. A TC+ x -> y C_ U_ x e. A TC+ x )
9		ttcid	|- y C_ TC+ y
10		ttceq	|- ( x = y -> TC+ x = TC+ y )
11	10	ssiun2s	|- ( y e. A -> TC+ y C_ U_ x e. A TC+ x )
12	9 11	sstrid	|- ( y e. A -> y C_ U_ x e. A TC+ x )
13	8 12	jaoi	|- ( ( y e. U_ x e. A TC+ x \/ y e. A ) -> y C_ U_ x e. A TC+ x )
14	3 13	sylbi	|- ( y e. ( U_ x e. A TC+ x u. A ) -> y C_ U_ x e. A TC+ x )
15		ssun3	|- ( y C_ U_ x e. A TC+ x -> y C_ ( U_ x e. A TC+ x u. A ) )
16	14 15	syl	|- ( y e. ( U_ x e. A TC+ x u. A ) -> y C_ ( U_ x e. A TC+ x u. A ) )
17	2 16	mprgbir	|- Tr ( U_ x e. A TC+ x u. A )
18		ttcmin	|- ( ( A C_ ( U_ x e. A TC+ x u. A ) /\ Tr ( U_ x e. A TC+ x u. A ) ) -> TC+ A C_ ( U_ x e. A TC+ x u. A ) )
19	1 17 18	mp2an	|- TC+ A C_ ( U_ x e. A TC+ x u. A )
20		iunss	|- ( U_ x e. A TC+ x C_ TC+ A <-> A. x e. A TC+ x C_ TC+ A )
21		ttcel2	|- ( x e. A -> TC+ x C_ TC+ A )
22	20 21	mprgbir	|- U_ x e. A TC+ x C_ TC+ A
23		ttcid	|- A C_ TC+ A
24	22 23	unssi	|- ( U_ x e. A TC+ x u. A ) C_ TC+ A
25	19 24	eqssi	|- TC+ A = ( U_ x e. A TC+ x u. A )