Metamath Proof Explorer

Theorem wffr

Description: The class of well-founded sets is well-founded. Lemma I.9.24(2) of Kunen2 p. 53. (Contributed by Eric Schmidt, 11-Oct-2025)

Ref Expression
Assertion wffr 
|- _E Fr U. ( R1 " On )

Proof

Step Hyp Ref Expression
1 rankrelp 
 |-  rank RelPres _E , _E ( U. ( R1 " On ) , On )
2 onfr 
 |-  _E Fr On
3 relpfr 
 |-  ( rank RelPres _E , _E ( U. ( R1 " On ) , On ) -> ( _E Fr On -> _E Fr U. ( R1 " On ) ) )
4 1 2 3 mp2 
 |-  _E Fr U. ( R1 " On )