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) (Proof revised by Scott Fenton, 18-Nov-2024.)

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 ) = frecs ( _E , On , ( F o. 2nd ) )
3 df-frecs 
 |-  frecs ( _E , On , ( F o. 2nd ) ) = 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 ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) }
4 3anass 
 |-  ( ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( 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 ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) ) )
5 vex 
 |-  x e. _V
6 5 elon 
 |-  ( x e. On <-> Ord x )
7 ordsson 
 |-  ( Ord x -> x C_ On )
8 ordtr 
 |-  ( Ord x -> Tr x )
9 7 8 jca 
 |-  ( Ord x -> ( x C_ On /\ Tr x ) )
10 epweon 
 |-  _E We On
11 wess 
 |-  ( x C_ On -> ( _E We On -> _E We x ) )
12 10 11 mpi 
 |-  ( x C_ On -> _E We x )
13 12 anim1ci 
 |-  ( ( x C_ On /\ Tr x ) -> ( Tr x /\ _E We x ) )
14 df-ord 
 |-  ( Ord x <-> ( Tr x /\ _E We x ) )
15 13 14 sylibr 
 |-  ( ( x C_ On /\ Tr x ) -> Ord x )
16 9 15 impbii 
 |-  ( Ord x <-> ( x C_ On /\ Tr x ) )
17 dftr3 
 |-  ( Tr x <-> A. y e. x y C_ x )
18 ssel2 
 |-  ( ( x C_ On /\ y e. x ) -> y e. On )
19 predon 
 |-  ( y e. On -> Pred ( _E , On , y ) = y )
20 19 sseq1d 
 |-  ( y e. On -> ( Pred ( _E , On , y ) C_ x <-> y C_ x ) )
21 18 20 syl 
 |-  ( ( x C_ On /\ y e. x ) -> ( Pred ( _E , On , y ) C_ x <-> y C_ x ) )
22 21 ralbidva 
 |-  ( x C_ On -> ( A. y e. x Pred ( _E , On , y ) C_ x <-> A. y e. x y C_ x ) )
23 17 22 bitr4id 
 |-  ( x C_ On -> ( Tr x <-> A. y e. x Pred ( _E , On , y ) C_ x ) )
24 23 pm5.32i 
 |-  ( ( x C_ On /\ Tr x ) <-> ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) )
25 6 16 24 3bitri 
 |-  ( x e. On <-> ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) )
26 25 anbi1i 
 |-  ( ( x e. On /\ A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) <-> ( ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) )
27 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
28 27 19 syl 
 |-  ( ( x e. On /\ y e. x ) -> Pred ( _E , On , y ) = y )
29 28 reseq2d 
 |-  ( ( x e. On /\ y e. x ) -> ( f |` Pred ( _E , On , y ) ) = ( f |` y ) )
30 29 oveq2d 
 |-  ( ( x e. On /\ y e. x ) -> ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) = ( y ( F o. 2nd ) ( f |` y ) ) )
31 id 
 |-  ( y e. x -> y e. x )
32 vex 
 |-  f e. _V
33 32 resex 
 |-  ( f |` y ) e. _V
34 33 a1i 
 |-  ( y e. x -> ( f |` y ) e. _V )
35 31 34 opco2 
 |-  ( y e. x -> ( y ( F o. 2nd ) ( f |` y ) ) = ( F ` ( f |` y ) ) )
36 35 adantl 
 |-  ( ( x e. On /\ y e. x ) -> ( y ( F o. 2nd ) ( f |` y ) ) = ( F ` ( f |` y ) ) )
37 30 36 eqtrd 
 |-  ( ( x e. On /\ y e. x ) -> ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) = ( F ` ( f |` y ) ) )
38 37 eqeq2d 
 |-  ( ( x e. On /\ y e. x ) -> ( ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) <-> ( f ` y ) = ( F ` ( f |` y ) ) ) )
39 38 ralbidva 
 |-  ( x e. On -> ( A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) <-> A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
40 39 pm5.32i 
 |-  ( ( x e. On /\ A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) <-> ( x e. On /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
41 26 40 bitr3i 
 |-  ( ( ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) <-> ( x e. On /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
42 41 anbi2i 
 |-  ( ( f Fn x /\ ( ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) ) <-> ( f Fn x /\ ( x e. On /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
43 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 ) ) ) ) )
44 4 42 43 3bitri 
 |-  ( ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) <-> ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
45 44 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 ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) <-> E. x ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
46 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 ) ) ) ) )
47 45 46 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 ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) <-> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
48 47 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 ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
49 48 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 ) = ( y ( F o. 2nd ) ( f |` Pred ( _E , On , y ) ) ) ) } = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
50 3 49 eqtri 
 |-  frecs ( _E , On , ( F o. 2nd ) ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
51 1 2 50 3eqtri 
 |-  recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }