Theorem ttcuni

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

	Ref	Expression
Assertion	ttcuni	Could not format assertion : No typesetting found for |- TC+ U. A = U. TC+ A with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ttcid	Could not format A C_ TC+ A : No typesetting found for |- A C_ TC+ A with typecode |-
2	1	unissi	Could not format U. A C_ U. TC+ A : No typesetting found for |- U. A C_ U. TC+ A with typecode |-
3		ttctr3	Could not format U. TC+ A C_ TC+ A : No typesetting found for |- U. TC+ A C_ TC+ A with typecode |-
4	3	unissi	Could not format U. U. TC+ A C_ U. TC+ A : No typesetting found for |- U. U. TC+ A C_ U. TC+ A with typecode |-
5		df-tr	Could not format ( Tr U. TC+ A <-> U. U. TC+ A C_ U. TC+ A ) : No typesetting found for |- ( Tr U. TC+ A <-> U. U. TC+ A C_ U. TC+ A ) with typecode |-
6	4 5	mpbir	Could not format Tr U. TC+ A : No typesetting found for |- Tr U. TC+ A with typecode |-
7		ttcmin	Could not format ( ( U. A C_ U. TC+ A /\ Tr U. TC+ A ) -> TC+ U. A C_ U. TC+ A ) : No typesetting found for |- ( ( U. A C_ U. TC+ A /\ Tr U. TC+ A ) -> TC+ U. A C_ U. TC+ A ) with typecode |-
8	2 6 7	mp2an	Could not format TC+ U. A C_ U. TC+ A : No typesetting found for |- TC+ U. A C_ U. TC+ A with typecode |-
9		ttcuniun	Could not format TC+ A = ( TC+ U. A u. A ) : No typesetting found for |- TC+ A = ( TC+ U. A u. A ) with typecode |-
10	9	unieqi	Could not format U. TC+ A = U. ( TC+ U. A u. A ) : No typesetting found for |- U. TC+ A = U. ( TC+ U. A u. A ) with typecode |-
11		uniun	Could not format U. ( TC+ U. A u. A ) = ( U. TC+ U. A u. U. A ) : No typesetting found for |- U. ( TC+ U. A u. A ) = ( U. TC+ U. A u. U. A ) with typecode |-
12	10 11	eqtri	Could not format U. TC+ A = ( U. TC+ U. A u. U. A ) : No typesetting found for |- U. TC+ A = ( U. TC+ U. A u. U. A ) with typecode |-
13		ttctr3	Could not format U. TC+ U. A C_ TC+ U. A : No typesetting found for |- U. TC+ U. A C_ TC+ U. A with typecode |-
14		ttcid	Could not format U. A C_ TC+ U. A : No typesetting found for |- U. A C_ TC+ U. A with typecode |-
15	13 14	unssi	Could not format ( U. TC+ U. A u. U. A ) C_ TC+ U. A : No typesetting found for |- ( U. TC+ U. A u. U. A ) C_ TC+ U. A with typecode |-
16	12 15	eqsstri	Could not format U. TC+ A C_ TC+ U. A : No typesetting found for |- U. TC+ A C_ TC+ U. A with typecode |-
17	8 16	eqssi	Could not format TC+ U. A = U. TC+ A : No typesetting found for |- TC+ U. A = U. TC+ A with typecode |-