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=wrecsRAG
Assertion wfr2a RWeARSeAXdomFFX=GFPredRAX

Proof

Step Hyp Ref Expression
1 wfrfun.1 F=wrecsRAG
2 wefr RWeARFrA
3 2 adantr RWeARSeARFrA
4 weso RWeAROrA
5 sopo ROrARPoA
6 4 5 syl RWeARPoA
7 6 adantr RWeARSeARPoA
8 simpr RWeARSeARSeA
9 3 7 8 3jca RWeARSeARFrARPoARSeA
10 df-wrecs wrecsRAG=frecsRAG2nd
11 1 10 eqtri F=frecsRAG2nd
12 11 fpr2a RFrARPoARSeAXdomFFX=XG2ndFPredRAX
13 9 12 sylan RWeARSeAXdomFFX=XG2ndFPredRAX
14 simpr RWeARSeAXdomFXdomF
15 1 wfrresex RWeARSeAXdomFFPredRAXV
16 14 15 opco2 RWeARSeAXdomFXG2ndFPredRAX=GFPredRAX
17 13 16 eqtrd RWeARSeAXdomFFX=GFPredRAX