Metamath Proof Explorer

Theorem fpr1

Description: Law of well-founded recursion over a partial order, part one. Establish the functionality and domain of the recursive function generator. Note that by requiring a partial order we can avoid using the axiom of infinity. (Contributed by Scott Fenton, 11-Sep-2023)

Ref Expression
Hypothesis fprr.1 
|- F = frecs ( R , A , G )
Assertion fpr1 
|- ( ( R Fr A /\ R Po A /\ R Se A ) -> F Fn A )

Proof

Step Hyp Ref Expression
1 fprr.1 
 |-  F = frecs ( R , A , G )
2 eqid 
 |-  { 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 G ( f |` Pred ( R , A , y ) ) ) ) } = { 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 G ( f |` Pred ( R , A , y ) ) ) ) }
3 2 frrlem1 
 |-  { 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 G ( f |` Pred ( R , A , y ) ) ) ) } = { a | E. b ( a Fn b /\ ( b C_ A /\ A. c e. b Pred ( R , A , c ) C_ b ) /\ A. c e. b ( a ` c ) = ( c G ( a |` Pred ( R , A , c ) ) ) ) }
4 3 1 fprlem1 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( g e. { 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 G ( f |` Pred ( R , A , y ) ) ) ) } /\ h e. { 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 G ( f |` Pred ( R , A , y ) ) ) ) } ) ) -> ( ( b g u /\ b h v ) -> u = v ) )
5 3 1 4 frrlem9 
 |-  ( ( R Fr A /\ R Po A /\ R Se A ) -> Fun F )
6 eqid 
 |-  ( ( F |` Pred ( R , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) = ( ( F |` Pred ( R , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } )
7 simp1 
 |-  ( ( R Fr A /\ R Po A /\ R Se A ) -> R Fr A )
8 ssidd 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) -> Pred ( R , A , z ) C_ Pred ( R , A , z ) )
9 fprlem2 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) -> A. y e. Pred ( R , A , z ) Pred ( R , A , y ) C_ Pred ( R , A , z ) )
10 setlikespec 
 |-  ( ( z e. A /\ R Se A ) -> Pred ( R , A , z ) e. _V )
11 10 ancoms 
 |-  ( ( R Se A /\ z e. A ) -> Pred ( R , A , z ) e. _V )
12 11 3ad2antl3 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) -> Pred ( R , A , z ) e. _V )
13 predss 
 |-  Pred ( R , A , z ) C_ A
14 13 a1i 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ z e. A ) -> Pred ( R , A , z ) C_ A )
15 difssd 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( A \ dom F ) =/= (/) ) -> ( A \ dom F ) C_ A )
16 simpr 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( A \ dom F ) =/= (/) ) -> ( A \ dom F ) =/= (/) )
17 15 16 jca 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( A \ dom F ) =/= (/) ) -> ( ( A \ dom F ) C_ A /\ ( A \ dom F ) =/= (/) ) )
18 frpomin2 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( ( A \ dom F ) C_ A /\ ( A \ dom F ) =/= (/) ) ) -> E. z e. ( A \ dom F ) Pred ( R , ( A \ dom F ) , z ) = (/) )
19 17 18 syldan 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( A \ dom F ) =/= (/) ) -> E. z e. ( A \ dom F ) Pred ( R , ( A \ dom F ) , z ) = (/) )
20 3 1 4 6 7 8 9 12 14 19 frrlem14 
 |-  ( ( R Fr A /\ R Po A /\ R Se A ) -> dom F = A )
21 df-fn 
 |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )
22 5 20 21 sylanbrc 
 |-  ( ( R Fr A /\ R Po A /\ R Se A ) -> F Fn A )