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

Metamath Proof Explorer

Theorem fprfung

Description: A "function" defined by well-founded recursion is indeed a function when the relation is a partial order. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 fprfung.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 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 ) ) ) ) } ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
4 2 1 3 frrlem9 
 |-  ( ( R Fr A /\ R Po A /\ R Se A ) -> Fun F )