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 ) ) ) )