Metamath Proof Explorer

Theorem ttciunun

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

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

Proof

Step Hyp Ref Expression
1 ssun2 Could not format A C_ ( U_ x e. A TC+ x u. A ) : No typesetting found for |- A C_ ( U_ x e. A TC+ x u. A ) with typecode |-
2 dftr3 Could not format ( Tr ( U_ x e. A TC+ x u. A ) <-> A. y e. ( U_ x e. A TC+ x u. A ) y C_ ( U_ x e. A TC+ x u. A ) ) : No typesetting found for |- ( Tr ( U_ x e. A TC+ x u. A ) <-> A. y e. ( U_ x e. A TC+ x u. A ) y C_ ( U_ x e. A TC+ x u. A ) ) with typecode |-
3 elun Could not format ( y e. ( U_ x e. A TC+ x u. A ) <-> ( y e. U_ x e. A TC+ x \/ y e. A ) ) : No typesetting found for |- ( y e. ( U_ x e. A TC+ x u. A ) <-> ( y e. U_ x e. A TC+ x \/ y e. A ) ) with typecode |-
4 ttctr Could not format Tr TC+ x : No typesetting found for |- Tr TC+ x with typecode |-
5 4 rgenw Could not format A. x e. A Tr TC+ x : No typesetting found for |- A. x e. A Tr TC+ x with typecode |-
6 triun Could not format ( A. x e. A Tr TC+ x -> Tr U_ x e. A TC+ x ) : No typesetting found for |- ( A. x e. A Tr TC+ x -> Tr U_ x e. A TC+ x ) with typecode |-
7 trss Could not format ( Tr U_ x e. A TC+ x -> ( y e. U_ x e. A TC+ x -> y C_ U_ x e. A TC+ x ) ) : No typesetting found for |- ( Tr U_ x e. A TC+ x -> ( y e. U_ x e. A TC+ x -> y C_ U_ x e. A TC+ x ) ) with typecode |-
8 5 6 7 mp2b Could not format ( y e. U_ x e. A TC+ x -> y C_ U_ x e. A TC+ x ) : No typesetting found for |- ( y e. U_ x e. A TC+ x -> y C_ U_ x e. A TC+ x ) with typecode |-
9 ttcid Could not format y C_ TC+ y : No typesetting found for |- y C_ TC+ y with typecode |-
10 ttceq Could not format ( x = y -> TC+ x = TC+ y ) : No typesetting found for |- ( x = y -> TC+ x = TC+ y ) with typecode |-
11 10 ssiun2s Could not format ( y e. A -> TC+ y C_ U_ x e. A TC+ x ) : No typesetting found for |- ( y e. A -> TC+ y C_ U_ x e. A TC+ x ) with typecode |-
12 9 11 sstrid Could not format ( y e. A -> y C_ U_ x e. A TC+ x ) : No typesetting found for |- ( y e. A -> y C_ U_ x e. A TC+ x ) with typecode |-
13 8 12 jaoi Could not format ( ( y e. U_ x e. A TC+ x \/ y e. A ) -> y C_ U_ x e. A TC+ x ) : No typesetting found for |- ( ( y e. U_ x e. A TC+ x \/ y e. A ) -> y C_ U_ x e. A TC+ x ) with typecode |-
14 3 13 sylbi Could not format ( y e. ( U_ x e. A TC+ x u. A ) -> y C_ U_ x e. A TC+ x ) : No typesetting found for |- ( y e. ( U_ x e. A TC+ x u. A ) -> y C_ U_ x e. A TC+ x ) with typecode |-
15 ssun3 Could not format ( y C_ U_ x e. A TC+ x -> y C_ ( U_ x e. A TC+ x u. A ) ) : No typesetting found for |- ( y C_ U_ x e. A TC+ x -> y C_ ( U_ x e. A TC+ x u. A ) ) with typecode |-
16 14 15 syl Could not format ( y e. ( U_ x e. A TC+ x u. A ) -> y C_ ( U_ x e. A TC+ x u. A ) ) : No typesetting found for |- ( y e. ( U_ x e. A TC+ x u. A ) -> y C_ ( U_ x e. A TC+ x u. A ) ) with typecode |-
17 2 16 mprgbir Could not format Tr ( U_ x e. A TC+ x u. A ) : No typesetting found for |- Tr ( U_ x e. A TC+ x u. A ) with typecode |-
18 ttcmin Could not format ( ( A C_ ( U_ x e. A TC+ x u. A ) /\ Tr ( U_ x e. A TC+ x u. A ) ) -> TC+ A C_ ( U_ x e. A TC+ x u. A ) ) : No typesetting found for |- ( ( A C_ ( U_ x e. A TC+ x u. A ) /\ Tr ( U_ x e. A TC+ x u. A ) ) -> TC+ A C_ ( U_ x e. A TC+ x u. A ) ) with typecode |-
19 1 17 18 mp2an Could not format TC+ A C_ ( U_ x e. A TC+ x u. A ) : No typesetting found for |- TC+ A C_ ( U_ x e. A TC+ x u. A ) with typecode |-
20 iunss Could not format ( U_ x e. A TC+ x C_ TC+ A <-> A. x e. A TC+ x C_ TC+ A ) : No typesetting found for |- ( U_ x e. A TC+ x C_ TC+ A <-> A. x e. A TC+ x C_ TC+ A ) with typecode |-
21 ttcel2 Could not format ( x e. A -> TC+ x C_ TC+ A ) : No typesetting found for |- ( x e. A -> TC+ x C_ TC+ A ) with typecode |-
22 20 21 mprgbir Could not format U_ x e. A TC+ x C_ TC+ A : No typesetting found for |- U_ x e. A TC+ x C_ TC+ A with typecode |-
23 ttcid Could not format A C_ TC+ A : No typesetting found for |- A C_ TC+ A with typecode |-
24 22 23 unssi Could not format ( U_ x e. A TC+ x u. A ) C_ TC+ A : No typesetting found for |- ( U_ x e. A TC+ x u. A ) C_ TC+ A with typecode |-
25 19 24 eqssi 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 |-