Theorem ttcun

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

	Ref	Expression
Assertion	ttcun	Could not format assertion : No typesetting found for |- TC+ ( A u. B ) = ( TC+ A u. TC+ B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		un4	Could not format ( ( U_ x e. A TC+ x u. U_ x e. B TC+ x ) u. ( A u. B ) ) = ( ( U_ x e. A TC+ x u. A ) u. ( U_ x e. B TC+ x u. B ) ) : No typesetting found for |- ( ( U_ x e. A TC+ x u. U_ x e. B TC+ x ) u. ( A u. B ) ) = ( ( U_ x e. A TC+ x u. A ) u. ( U_ x e. B TC+ x u. B ) ) with typecode |-
2		ttciunun	Could not format TC+ ( A u. B ) = ( U_ x e. ( A u. B ) TC+ x u. ( A u. B ) ) : No typesetting found for |- TC+ ( A u. B ) = ( U_ x e. ( A u. B ) TC+ x u. ( A u. B ) ) with typecode |-
3		iunxun	Could not format U_ x e. ( A u. B ) TC+ x = ( U_ x e. A TC+ x u. U_ x e. B TC+ x ) : No typesetting found for |- U_ x e. ( A u. B ) TC+ x = ( U_ x e. A TC+ x u. U_ x e. B TC+ x ) with typecode |-
4	3	uneq1i	Could not format ( U_ x e. ( A u. B ) TC+ x u. ( A u. B ) ) = ( ( U_ x e. A TC+ x u. U_ x e. B TC+ x ) u. ( A u. B ) ) : No typesetting found for |- ( U_ x e. ( A u. B ) TC+ x u. ( A u. B ) ) = ( ( U_ x e. A TC+ x u. U_ x e. B TC+ x ) u. ( A u. B ) ) with typecode |-
5	2 4	eqtri	Could not format TC+ ( A u. B ) = ( ( U_ x e. A TC+ x u. U_ x e. B TC+ x ) u. ( A u. B ) ) : No typesetting found for |- TC+ ( A u. B ) = ( ( U_ x e. A TC+ x u. U_ x e. B TC+ x ) u. ( A u. B ) ) with typecode |-
6		ttciunun	Could not format TC+ A = ( U_ x e. A TC+ x u. A ) : No typesetting found for |- TC+ A = ( U_ x e. A TC+ x u. A ) with typecode |-
7		ttciunun	Could not format TC+ B = ( U_ x e. B TC+ x u. B ) : No typesetting found for |- TC+ B = ( U_ x e. B TC+ x u. B ) with typecode |-
8	6 7	uneq12i	Could not format ( TC+ A u. TC+ B ) = ( ( U_ x e. A TC+ x u. A ) u. ( U_ x e. B TC+ x u. B ) ) : No typesetting found for |- ( TC+ A u. TC+ B ) = ( ( U_ x e. A TC+ x u. A ) u. ( U_ x e. B TC+ x u. B ) ) with typecode |-
9	1 5 8	3eqtr4i	Could not format TC+ ( A u. B ) = ( TC+ A u. TC+ B ) : No typesetting found for |- TC+ ( A u. B ) = ( TC+ A u. TC+ B ) with typecode |-