Metamath Proof Explorer


Definition df-wrecs

Description: Here we define the well-ordered recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function F , a relationship R , and a base set A , this definition generates a function G = wrecs ( R , A , F ) that has property that, at any point x e. A , ( Gx ) = ( F` ( G |`Pred ( R , A , x ) ) ) . See wfr1 , wfr2 , and wfr3 . (Contributed by Scott Fenton, 7-Jun-2018) (New usage is discouraged.)

Ref Expression
Assertion df-wrecs
|- wrecs ( R , A , F ) = U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR
 |-  R
1 cA
 |-  A
2 cF
 |-  F
3 1 0 2 cwrecs
 |-  wrecs ( R , A , F )
4 vf
 |-  f
5 vx
 |-  x
6 4 cv
 |-  f
7 5 cv
 |-  x
8 6 7 wfn
 |-  f Fn x
9 7 1 wss
 |-  x C_ A
10 vy
 |-  y
11 10 cv
 |-  y
12 1 0 11 cpred
 |-  Pred ( R , A , y )
13 12 7 wss
 |-  Pred ( R , A , y ) C_ x
14 13 10 7 wral
 |-  A. y e. x Pred ( R , A , y ) C_ x
15 9 14 wa
 |-  ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x )
16 11 6 cfv
 |-  ( f ` y )
17 6 12 cres
 |-  ( f |` Pred ( R , A , y ) )
18 17 2 cfv
 |-  ( F ` ( f |` Pred ( R , A , y ) ) )
19 16 18 wceq
 |-  ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
20 19 10 7 wral
 |-  A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) )
21 8 15 20 w3a
 |-  ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) )
22 21 5 wex
 |-  E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) )
23 22 4 cab
 |-  { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
24 23 cuni
 |-  U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
25 3 24 wceq
 |-  wrecs ( R , A , F ) = U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }