Metamath Proof Explorer

Theorem dfrecs3

Description: The old definition of transfinite recursion. This version is preferred for development, as it demonstrates the properties of transfinite recursion without relying on well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020)

Ref Expression
Assertion dfrecs3 
|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }

Proof

Step Hyp Ref Expression
1 df-recs 
 |-  recs ( F ) = wrecs ( _E , On , F )
2 df-wrecs 
 |-  wrecs ( _E , On , F ) = U. { f | E. x ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) }
3 3anass 
 |-  ( ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) <-> ( f Fn x /\ ( ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) ) )
4 vex 
 |-  x e. _V
5 4 elon 
 |-  ( x e. On <-> Ord x )
6 ordsson 
 |-  ( Ord x -> x C_ On )
7 ordtr 
 |-  ( Ord x -> Tr x )
8 6 7 jca 
 |-  ( Ord x -> ( x C_ On /\ Tr x ) )
9 epweon 
 |-  _E We On
10 wess 
 |-  ( x C_ On -> ( _E We On -> _E We x ) )
11 9 10 mpi 
 |-  ( x C_ On -> _E We x )
12 11 anim1ci 
 |-  ( ( x C_ On /\ Tr x ) -> ( Tr x /\ _E We x ) )
13 df-ord 
 |-  ( Ord x <-> ( Tr x /\ _E We x ) )
14 12 13 sylibr 
 |-  ( ( x C_ On /\ Tr x ) -> Ord x )
15 8 14 impbii 
 |-  ( Ord x <-> ( x C_ On /\ Tr x ) )
16 dftr3 
 |-  ( Tr x <-> A. y e. x y C_ x )
17 ssel2 
 |-  ( ( x C_ On /\ y e. x ) -> y e. On )
18 predon 
 |-  ( y e. On -> Pred ( _E , On , y ) = y )
19 18 sseq1d 
 |-  ( y e. On -> ( Pred ( _E , On , y ) C_ x <-> y C_ x ) )
20 17 19 syl 
 |-  ( ( x C_ On /\ y e. x ) -> ( Pred ( _E , On , y ) C_ x <-> y C_ x ) )
21 20 ralbidva 
 |-  ( x C_ On -> ( A. y e. x Pred ( _E , On , y ) C_ x <-> A. y e. x y C_ x ) )
22 16 21 bitr4id 
 |-  ( x C_ On -> ( Tr x <-> A. y e. x Pred ( _E , On , y ) C_ x ) )
23 22 pm5.32i 
 |-  ( ( x C_ On /\ Tr x ) <-> ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) )
24 5 15 23 3bitri 
 |-  ( x e. On <-> ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) )
25 24 anbi1i 
 |-  ( ( x e. On /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) <-> ( ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) )
26 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
27 18 reseq2d 
 |-  ( y e. On -> ( f |` Pred ( _E , On , y ) ) = ( f |` y ) )
28 27 fveq2d 
 |-  ( y e. On -> ( F ` ( f |` Pred ( _E , On , y ) ) ) = ( F ` ( f |` y ) ) )
29 28 eqeq2d 
 |-  ( y e. On -> ( ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) <-> ( f ` y ) = ( F ` ( f |` y ) ) ) )
30 26 29 syl 
 |-  ( ( x e. On /\ y e. x ) -> ( ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) <-> ( f ` y ) = ( F ` ( f |` y ) ) ) )
31 30 ralbidva 
 |-  ( x e. On -> ( A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) <-> A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
32 31 pm5.32i 
 |-  ( ( x e. On /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) <-> ( x e. On /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
33 25 32 bitr3i 
 |-  ( ( ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) <-> ( x e. On /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
34 33 anbi2i 
 |-  ( ( f Fn x /\ ( ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) ) <-> ( f Fn x /\ ( x e. On /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
35 an12 
 |-  ( ( f Fn x /\ ( x e. On /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) <-> ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
36 3 34 35 3bitri 
 |-  ( ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) <-> ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
37 36 exbii 
 |-  ( E. x ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) <-> E. x ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
38 df-rex 
 |-  ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) <-> E. x ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
39 37 38 bitr4i 
 |-  ( E. x ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) <-> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
40 39 abbii 
 |-  { f | E. x ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
41 40 unieqi 
 |-  U. { f | E. x ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( _E , On , y ) ) ) ) } = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
42 1 2 41 3eqtri 
 |-  recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }