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

Metamath Proof Explorer

Theorem wfr2a

Description: A weak version of wfr2 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Scott Fenton, 30-Jul-2020) (Proof shortened by Scott Fenton, 18-Nov-2024)

Ref Expression
Hypothesis wfrfun.1 
|- F = wrecs ( R , A , G )
Assertion wfr2a 
|- ( ( ( R We A /\ R Se A ) /\ X e. dom F ) -> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )

Proof

Step Hyp Ref Expression
1 wfrfun.1 
 |-  F = wrecs ( R , A , G )
2 wefr 
 |-  ( R We A -> R Fr A )
3 2 adantr 
 |-  ( ( R We A /\ R Se A ) -> R Fr A )
4 weso 
 |-  ( R We A -> R Or A )
5 sopo 
 |-  ( R Or A -> R Po A )
6 4 5 syl 
 |-  ( R We A -> R Po A )
7 6 adantr 
 |-  ( ( R We A /\ R Se A ) -> R Po A )
8 simpr 
 |-  ( ( R We A /\ R Se A ) -> R Se A )
9 3 7 8 3jca 
 |-  ( ( R We A /\ R Se A ) -> ( R Fr A /\ R Po A /\ R Se A ) )
10 df-wrecs 
 |-  wrecs ( R , A , G ) = frecs ( R , A , ( G o. 2nd ) )
11 1 10 eqtri 
 |-  F = frecs ( R , A , ( G o. 2nd ) )
12 11 fpr2a 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ X e. dom F ) -> ( F ` X ) = ( X ( G o. 2nd ) ( F |` Pred ( R , A , X ) ) ) )
13 9 12 sylan 
 |-  ( ( ( R We A /\ R Se A ) /\ X e. dom F ) -> ( F ` X ) = ( X ( G o. 2nd ) ( F |` Pred ( R , A , X ) ) ) )
14 simpr 
 |-  ( ( ( R We A /\ R Se A ) /\ X e. dom F ) -> X e. dom F )
15 1 wfrresex 
 |-  ( ( ( R We A /\ R Se A ) /\ X e. dom F ) -> ( F |` Pred ( R , A , X ) ) e. _V )
16 14 15 opco2 
 |-  ( ( ( R We A /\ R Se A ) /\ X e. dom F ) -> ( X ( G o. 2nd ) ( F |` Pred ( R , A , X ) ) ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )
17 13 16 eqtrd 
 |-  ( ( ( R We A /\ R Se A ) /\ X e. dom F ) -> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )