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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rankrelp | Could not format rank RelPres _E , _E ( U. ( R1 " On ) , On ) : No typesetting found for |- rank RelPres _E , _E ( U. ( R1 " On ) , On ) with typecode |- | |
2 | onfr | ||
3 | relpfr | Could not format ( rank RelPres _E , _E ( U. ( R1 " On ) , On ) -> ( _E Fr On -> _E Fr U. ( R1 " On ) ) ) : No typesetting found for |- ( rank RelPres _E , _E ( U. ( R1 " On ) , On ) -> ( _E Fr On -> _E Fr U. ( R1 " On ) ) ) with typecode |- | |
4 | 1 2 3 | mp2 |