Metamath Proof Explorer

Theorem dfttc2g

Description: A shorter expression for the transitive closure of a set. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion dfttc2g 
|- ( A e. V -> TC+ A = U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )

Proof

Step Hyp Ref Expression
1 rdg0g 
 |-  ( A e. V -> ( rec ( ( x e. _V |-> U. x ) , A ) ` (/) ) = A )
2 rdgfnon 
 |-  rec ( ( x e. _V |-> U. x ) , A ) Fn On
3 omsson 
 |-  _om C_ On
4 peano1 
 |-  (/) e. _om
5 fnfvima 
 |-  ( ( rec ( ( x e. _V |-> U. x ) , A ) Fn On /\ _om C_ On /\ (/) e. _om ) -> ( rec ( ( x e. _V |-> U. x ) , A ) ` (/) ) e. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )
6 2 3 4 5 mp3an 
 |-  ( rec ( ( x e. _V |-> U. x ) , A ) ` (/) ) e. ( rec ( ( x e. _V |-> U. x ) , A ) " _om )
7 1 6 eqeltrrdi 
 |-  ( A e. V -> A e. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )
8 elssuni 
 |-  ( A e. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) -> A C_ U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )
9 7 8 syl 
 |-  ( A e. V -> A C_ U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )
10 peano2 
 |-  ( z e. _om -> suc z e. _om )
11 elunii 
 |-  ( ( w e. y /\ y e. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) ) -> w e. U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) )
12 nnon 
 |-  ( z e. _om -> z e. On )
13 fvex 
 |-  ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) e. _V
14 13 uniex 
 |-  U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) e. _V
15 eqid 
 |-  rec ( ( x e. _V |-> U. x ) , A ) = rec ( ( x e. _V |-> U. x ) , A )
16 unieq 
 |-  ( y = x -> U. y = U. x )
17 unieq 
 |-  ( y = ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) -> U. y = U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) )
18 15 16 17 rdgsucmpt2 
 |-  ( ( z e. On /\ U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) e. _V ) -> ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) = U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) )
19 12 14 18 sylancl 
 |-  ( z e. _om -> ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) = U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) )
20 19 eleq2d 
 |-  ( z e. _om -> ( w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) <-> w e. U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) ) )
21 20 biimpar 
 |-  ( ( z e. _om /\ w e. U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) ) -> w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) )
22 11 21 sylan2 
 |-  ( ( z e. _om /\ ( w e. y /\ y e. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) ) ) -> w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) )
23 fveq2 
 |-  ( y = suc z -> ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) = ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) )
24 23 eleq2d 
 |-  ( y = suc z -> ( w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) <-> w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) ) )
25 24 rspcev 
 |-  ( ( suc z e. _om /\ w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) ) -> E. y e. _om w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) )
26 10 22 25 syl2an2r 
 |-  ( ( z e. _om /\ ( w e. y /\ y e. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) ) ) -> E. y e. _om w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) )
27 26 an12s 
 |-  ( ( w e. y /\ ( z e. _om /\ y e. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) ) ) -> E. y e. _om w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) )
28 27 rexlimdvaa 
 |-  ( w e. y -> ( E. z e. _om y e. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) -> E. y e. _om w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) ) )
29 rdgfun 
 |-  Fun rec ( ( x e. _V |-> U. x ) , A )
30 eluniima 
 |-  ( Fun rec ( ( x e. _V |-> U. x ) , A ) -> ( y e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) <-> E. z e. _om y e. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) ) )
31 29 30 ax-mp 
 |-  ( y e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) <-> E. z e. _om y e. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) )
32 eluniima 
 |-  ( Fun rec ( ( x e. _V |-> U. x ) , A ) -> ( w e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) <-> E. y e. _om w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) ) )
33 29 32 ax-mp 
 |-  ( w e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) <-> E. y e. _om w e. ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) )
34 28 31 33 3imtr4g 
 |-  ( w e. y -> ( y e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) -> w e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) ) )
35 34 imp 
 |-  ( ( w e. y /\ y e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) ) -> w e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )
36 35 gen2 
 |-  A. w A. y ( ( w e. y /\ y e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) ) -> w e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )
37 dftr2 
 |-  ( Tr U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) <-> A. w A. y ( ( w e. y /\ y e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) ) -> w e. U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) ) )
38 36 37 mpbir 
 |-  Tr U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om )
39 ttcmin 
 |-  ( ( A C_ U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) /\ Tr U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) ) -> TC+ A C_ U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )
40 9 38 39 sylancl 
 |-  ( A e. V -> TC+ A C_ U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )
41 funiunfv 
 |-  ( Fun rec ( ( x e. _V |-> U. x ) , A ) -> U_ y e. _om ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) = U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )
42 29 41 ax-mp 
 |-  U_ y e. _om ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) = U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om )
43 fveq2 
 |-  ( y = (/) -> ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) = ( rec ( ( x e. _V |-> U. x ) , A ) ` (/) ) )
44 43 sseq1d 
 |-  ( y = (/) -> ( ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) C_ TC+ A <-> ( rec ( ( x e. _V |-> U. x ) , A ) ` (/) ) C_ TC+ A ) )
45 fveq2 
 |-  ( y = z -> ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) = ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) )
46 45 sseq1d 
 |-  ( y = z -> ( ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) C_ TC+ A <-> ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) C_ TC+ A ) )
47 23 sseq1d 
 |-  ( y = suc z -> ( ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) C_ TC+ A <-> ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) C_ TC+ A ) )
48 ttcid 
 |-  A C_ TC+ A
49 1 48 eqsstrdi 
 |-  ( A e. V -> ( rec ( ( x e. _V |-> U. x ) , A ) ` (/) ) C_ TC+ A )
50 uniss 
 |-  ( ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) C_ TC+ A -> U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) C_ U. TC+ A )
51 ttctr3 
 |-  U. TC+ A C_ TC+ A
52 50 51 sstrdi 
 |-  ( ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) C_ TC+ A -> U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) C_ TC+ A )
53 19 sseq1d 
 |-  ( z e. _om -> ( ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) C_ TC+ A <-> U. ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) C_ TC+ A ) )
54 52 53 imbitrrid 
 |-  ( z e. _om -> ( ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) C_ TC+ A -> ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) C_ TC+ A ) )
55 54 a1d 
 |-  ( z e. _om -> ( A e. V -> ( ( rec ( ( x e. _V |-> U. x ) , A ) ` z ) C_ TC+ A -> ( rec ( ( x e. _V |-> U. x ) , A ) ` suc z ) C_ TC+ A ) ) )
56 44 46 47 49 55 finds2 
 |-  ( y e. _om -> ( A e. V -> ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) C_ TC+ A ) )
57 56 impcom 
 |-  ( ( A e. V /\ y e. _om ) -> ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) C_ TC+ A )
58 57 iunssd 
 |-  ( A e. V -> U_ y e. _om ( rec ( ( x e. _V |-> U. x ) , A ) ` y ) C_ TC+ A )
59 42 58 eqsstrrid 
 |-  ( A e. V -> U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) C_ TC+ A )
60 40 59 eqssd 
 |-  ( A e. V -> TC+ A = U. ( rec ( ( x e. _V |-> U. x ) , A ) " _om ) )