Metamath Proof Explorer

Theorem ttcid

Description: The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion ttcid 
|- A C_ TC+ A

Proof

Step Hyp Ref Expression
1 vsnid 
 |-  z e. { z }
2 vsnex 
 |-  { z } e. _V
3 2 rdg0 
 |-  ( rec ( ( y e. _V |-> U. y ) , { z } ) ` (/) ) = { z }
4 rdgfnon 
 |-  rec ( ( y e. _V |-> U. y ) , { z } ) Fn On
5 omsson 
 |-  _om C_ On
6 peano1 
 |-  (/) e. _om
7 fnfvima 
 |-  ( ( rec ( ( y e. _V |-> U. y ) , { z } ) Fn On /\ _om C_ On /\ (/) e. _om ) -> ( rec ( ( y e. _V |-> U. y ) , { z } ) ` (/) ) e. ( rec ( ( y e. _V |-> U. y ) , { z } ) " _om ) )
8 4 5 6 7 mp3an 
 |-  ( rec ( ( y e. _V |-> U. y ) , { z } ) ` (/) ) e. ( rec ( ( y e. _V |-> U. y ) , { z } ) " _om )
9 3 8 eqeltrri 
 |-  { z } e. ( rec ( ( y e. _V |-> U. y ) , { z } ) " _om )
10 elunii 
 |-  ( ( z e. { z } /\ { z } e. ( rec ( ( y e. _V |-> U. y ) , { z } ) " _om ) ) -> z e. U. ( rec ( ( y e. _V |-> U. y ) , { z } ) " _om ) )
11 1 9 10 mp2an 
 |-  z e. U. ( rec ( ( y e. _V |-> U. y ) , { z } ) " _om )
12 sneq 
 |-  ( x = z -> { x } = { z } )
13 rdgeq2 
 |-  ( { x } = { z } -> rec ( ( y e. _V |-> U. y ) , { x } ) = rec ( ( y e. _V |-> U. y ) , { z } ) )
14 12 13 syl 
 |-  ( x = z -> rec ( ( y e. _V |-> U. y ) , { x } ) = rec ( ( y e. _V |-> U. y ) , { z } ) )
15 14 imaeq1d 
 |-  ( x = z -> ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) = ( rec ( ( y e. _V |-> U. y ) , { z } ) " _om ) )
16 15 unieqd 
 |-  ( x = z -> U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) = U. ( rec ( ( y e. _V |-> U. y ) , { z } ) " _om ) )
17 16 eliuni 
 |-  ( ( z e. A /\ z e. U. ( rec ( ( y e. _V |-> U. y ) , { z } ) " _om ) ) -> z e. U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
18 11 17 mpan2 
 |-  ( z e. A -> z e. U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
19 df-ttc 
 |-  TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )
20 18 19 eleqtrrdi 
 |-  ( z e. A -> z e. TC+ A )
21 20 ssriv 
 |-  A C_ TC+ A