Metamath Proof Explorer

Theorem ttctr

Description: The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion ttctr 
|- Tr TC+ A

Proof

Step Hyp Ref Expression
1 rdgfun 
 |-  Fun rec ( ( y e. _V |-> U. y ) , { x } )
2 eluniima 
 |-  ( Fun rec ( ( y e. _V |-> U. y ) , { x } ) -> ( v e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) <-> E. z e. _om v e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) ) )
3 1 2 ax-mp 
 |-  ( v e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) <-> E. z e. _om v e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) )
4 peano2 
 |-  ( z e. _om -> suc z e. _om )
5 elunii 
 |-  ( ( u e. v /\ v e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) ) -> u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) )
6 nnon 
 |-  ( z e. _om -> z e. On )
7 fvex 
 |-  ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) e. _V
8 7 uniex 
 |-  U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) e. _V
9 eqid 
 |-  rec ( ( y e. _V |-> U. y ) , { x } ) = rec ( ( y e. _V |-> U. y ) , { x } )
10 unieq 
 |-  ( w = y -> U. w = U. y )
11 unieq 
 |-  ( w = ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) -> U. w = U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) )
12 9 10 11 rdgsucmpt2 
 |-  ( ( z e. On /\ U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) e. _V ) -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc z ) = U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) )
13 6 8 12 sylancl 
 |-  ( z e. _om -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc z ) = U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) )
14 13 eleq2d 
 |-  ( z e. _om -> ( u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc z ) <-> u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) ) )
15 14 biimpar 
 |-  ( ( z e. _om /\ u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) ) -> u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc z ) )
16 5 15 sylan2 
 |-  ( ( z e. _om /\ ( u e. v /\ v e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) ) ) -> u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc z ) )
17 fveq2 
 |-  ( w = suc z -> ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) = ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc z ) )
18 17 eleq2d 
 |-  ( w = suc z -> ( u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) <-> u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc z ) ) )
19 18 rspcev 
 |-  ( ( suc z e. _om /\ u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` suc z ) ) -> E. w e. _om u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) )
20 4 16 19 syl2an2r 
 |-  ( ( z e. _om /\ ( u e. v /\ v e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) ) ) -> E. w e. _om u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) )
21 eluniima 
 |-  ( Fun rec ( ( y e. _V |-> U. y ) , { x } ) -> ( u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) <-> E. w e. _om u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) ) )
22 1 21 ax-mp 
 |-  ( u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) <-> E. w e. _om u e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` w ) )
23 20 22 sylibr 
 |-  ( ( z e. _om /\ ( u e. v /\ v e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) ) ) -> u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
24 23 an12s 
 |-  ( ( u e. v /\ ( z e. _om /\ v e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) ) ) -> u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
25 24 rexlimdvaa 
 |-  ( u e. v -> ( E. z e. _om v e. ( rec ( ( y e. _V |-> U. y ) , { x } ) ` z ) -> u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) ) )
26 3 25 biimtrid 
 |-  ( u e. v -> ( v e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) -> u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) ) )
27 26 reximdv 
 |-  ( u e. v -> ( E. x e. A v e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) -> E. x e. A u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) ) )
28 eliun 
 |-  ( v e. U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) <-> E. x e. A v e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
29 eliun 
 |-  ( u e. U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) <-> E. x e. A u e. U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
30 27 28 29 3imtr4g 
 |-  ( u e. v -> ( v e. U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) -> u e. U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) ) )
31 df-ttc 
 |-  TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )
32 31 eleq2i 
 |-  ( v e. TC+ A <-> v e. U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
33 31 eleq2i 
 |-  ( u e. TC+ A <-> u e. U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
34 30 32 33 3imtr4g 
 |-  ( u e. v -> ( v e. TC+ A -> u e. TC+ A ) )
35 34 imp 
 |-  ( ( u e. v /\ v e. TC+ A ) -> u e. TC+ A )
36 35 gen2 
 |-  A. u A. v ( ( u e. v /\ v e. TC+ A ) -> u e. TC+ A )
37 dftr2 
 |-  ( Tr TC+ A <-> A. u A. v ( ( u e. v /\ v e. TC+ A ) -> u e. TC+ A ) )
38 36 37 mpbir 
 |-  Tr TC+ A