Theorem ttciun

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

	Ref	Expression
Assertion	ttciun	Could not format assertion : No typesetting found for |- TC+ U_ x e. A B = U_ x e. A TC+ B with typecode |-

Proof

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