Metamath Proof Explorer

Theorem ttcun

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

Ref Expression
Assertion ttcun 
|- TC+ ( A u. B ) = ( TC+ A u. TC+ B )

Proof

Step Hyp Ref Expression
1 un4 
 |-  ( ( 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 ) )
2 ttciunun 
 |-  TC+ ( A u. B ) = ( U_ x e. ( A u. B ) TC+ x u. ( A u. B ) )
3 iunxun 
 |-  U_ x e. ( A u. B ) TC+ x = ( U_ x e. A TC+ x u. U_ x e. B TC+ x )
4 3 uneq1i 
 |-  ( 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 ) )
5 2 4 eqtri 
 |-  TC+ ( A u. B ) = ( ( U_ x e. A TC+ x u. U_ x e. B TC+ x ) u. ( A u. B ) )
6 ttciunun 
 |-  TC+ A = ( U_ x e. A TC+ x u. A )
7 ttciunun 
 |-  TC+ B = ( U_ x e. B TC+ x u. B )
8 6 7 uneq12i 
 |-  ( TC+ A u. TC+ B ) = ( ( U_ x e. A TC+ x u. A ) u. ( U_ x e. B TC+ x u. B ) )
9 1 5 8 3eqtr4i 
 |-  TC+ ( A u. B ) = ( TC+ A u. TC+ B )