Metamath Proof Explorer

Theorem fpr2a

Description: Weak version of fpr2 which is useful for proofs that avoid the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024)

Ref Expression
Hypothesis fpr2a.1 
|- F = frecs ( R , A , G )
Assertion fpr2a 
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ X e. dom F ) -> ( F ` X ) = ( X G ( F |` Pred ( R , A , X ) ) ) )

Proof

Step Hyp Ref Expression
1 fpr2a.1 
 |-  F = frecs ( R , A , G )
2 fveq2 
 |-  ( y = X -> ( F ` y ) = ( F ` X ) )
3 id 
 |-  ( y = X -> y = X )
4 predeq3 
 |-  ( y = X -> Pred ( R , A , y ) = Pred ( R , A , X ) )
5 4 reseq2d 
 |-  ( y = X -> ( F |` Pred ( R , A , y ) ) = ( F |` Pred ( R , A , X ) ) )
6 3 5 oveq12d 
 |-  ( y = X -> ( y G ( F |` Pred ( R , A , y ) ) ) = ( X G ( F |` Pred ( R , A , X ) ) ) )
7 2 6 eqeq12d 
 |-  ( y = X -> ( ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) <-> ( F ` X ) = ( X G ( F |` Pred ( R , A , X ) ) ) ) )
8 7 imbi2d 
 |-  ( y = X -> ( ( ( R Fr A /\ R Po A /\ R Se A ) -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) ) <-> ( ( R Fr A /\ R Po A /\ R Se A ) -> ( F ` X ) = ( X G ( F |` Pred ( R , A , X ) ) ) ) ) )
9 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 ) ) ) ) }
10 9 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 ) )
11 9 1 10 frrlem10 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ y e. dom F ) -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) )
12 11 expcom 
 |-  ( y e. dom F -> ( ( R Fr A /\ R Po A /\ R Se A ) -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) ) )
13 8 12 vtoclga 
 |-  ( X e. dom F -> ( ( R Fr A /\ R Po A /\ R Se A ) -> ( F ` X ) = ( X G ( F |` Pred ( R , A , X ) ) ) ) )
14 13 impcom 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ X e. dom F ) -> ( F ` X ) = ( X G ( F |` Pred ( R , A , X ) ) ) )