Metamath Proof Explorer

Theorem ttcuniun

Description: Relationship between TC+ A and TC+ U. A : we can decompose TC+ A into the elements of TC+ U. A plus the elements of A itself. (Contributed by Matthew House, 6-Apr-2026)

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

Proof

Step Hyp Ref Expression
1 ssun2 Could not format A C_ ( TC+ U. A u. A ) : No typesetting found for |- A C_ ( TC+ U. A u. A ) with typecode |-
2 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 |-
3 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 |-
4 ttcid Could not format U. A C_ TC+ U. A : No typesetting found for |- U. A C_ TC+ U. A with typecode |-
5 3 4 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 |-
6 2 5 eqsstri Could not format U. ( TC+ U. A u. A ) C_ TC+ U. A : No typesetting found for |- U. ( TC+ U. A u. A ) C_ TC+ U. A with typecode |-
7 ssun3 Could not format ( U. ( TC+ U. A u. A ) C_ TC+ U. A -> U. ( TC+ U. A u. A ) C_ ( TC+ U. A u. A ) ) : No typesetting found for |- ( U. ( TC+ U. A u. A ) C_ TC+ U. A -> U. ( TC+ U. A u. A ) C_ ( TC+ U. A u. A ) ) with typecode |-
8 6 7 ax-mp Could not format U. ( TC+ U. A u. A ) C_ ( TC+ U. A u. A ) : No typesetting found for |- U. ( TC+ U. A u. A ) C_ ( TC+ U. A u. A ) with typecode |-
9 df-tr Could not format ( Tr ( TC+ U. A u. A ) <-> U. ( TC+ U. A u. A ) C_ ( TC+ U. A u. A ) ) : No typesetting found for |- ( Tr ( TC+ U. A u. A ) <-> U. ( TC+ U. A u. A ) C_ ( TC+ U. A u. A ) ) with typecode |-
10 8 9 mpbir Could not format Tr ( TC+ U. A u. A ) : No typesetting found for |- Tr ( TC+ U. A u. A ) with typecode |-
11 ttcmin Could not format ( ( A C_ ( TC+ U. A u. A ) /\ Tr ( TC+ U. A u. A ) ) -> TC+ A C_ ( TC+ U. A u. A ) ) : No typesetting found for |- ( ( A C_ ( TC+ U. A u. A ) /\ Tr ( TC+ U. A u. A ) ) -> TC+ A C_ ( TC+ U. A u. A ) ) with typecode |-
12 1 10 11 mp2an Could not format TC+ A C_ ( TC+ U. A u. A ) : No typesetting found for |- TC+ A C_ ( TC+ U. A u. A ) with typecode |-
13 ttcid Could not format A C_ TC+ A : No typesetting found for |- A C_ TC+ A with typecode |-
14 13 unissi Could not format U. A C_ U. TC+ A : No typesetting found for |- U. A C_ U. TC+ A with typecode |-
15 ttctr3 Could not format U. TC+ A C_ TC+ A : No typesetting found for |- U. TC+ A C_ TC+ A with typecode |-
16 14 15 sstri Could not format U. A C_ TC+ A : No typesetting found for |- U. A C_ TC+ A with typecode |-
17 ttcss Could not format ( U. A C_ TC+ A -> TC+ U. A C_ TC+ A ) : No typesetting found for |- ( U. A C_ TC+ A -> TC+ U. A C_ TC+ A ) with typecode |-
18 16 17 ax-mp Could not format TC+ U. A C_ TC+ A : No typesetting found for |- TC+ U. A C_ TC+ A with typecode |-
19 18 13 unssi Could not format ( TC+ U. A u. A ) C_ TC+ A : No typesetting found for |- ( TC+ U. A u. A ) C_ TC+ A with typecode |-
20 12 19 eqssi Could not format TC+ A = ( TC+ U. A u. A ) : No typesetting found for |- TC+ A = ( TC+ U. A u. A ) with typecode |-