This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-frecs

Description: This is the definition for the well-founded recursion generator. Similar to df-wrecs and df-recs , it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a well-founded set-like relationship for its properties, not a well-ordered relationship. This proof requires either a partial order or the axiom of infinity. We develop the theorems twice, once with a partial order and once without. The second development occurs later in the database, after ax-inf has been introduced. (Contributed by Scott Fenton, 23-Dec-2021)

Ref Expression
Assertion df-frecs 
|- frecs ( 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 ) = ( 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 cfrecs 
 |-  frecs ( 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 11 17 2 co 
 |-  ( y F ( f |` Pred ( R , A , y ) ) )
19 16 18 wceq 
 |-  ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) )
20 19 10 7 wral 
 |-  A. y e. x ( f ` y ) = ( 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 ) = ( 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 ) = ( 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 ) = ( 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 ) = ( y F ( f |` Pred ( R , A , y ) ) ) ) }
25 3 24 wceq 
 |-  frecs ( 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 ) = ( y F ( f |` Pred ( R , A , y ) ) ) ) }