Description: A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr . (Contributed by Mario Carneiro, 2-Jan-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wfelirr | |- ( A e. U. ( R1 " On ) -> -. A e. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rankon | |- ( rank ` A ) e. On |
|
| 2 | 1 | onirri | |- -. ( rank ` A ) e. ( rank ` A ) |
| 3 | rankelb | |- ( A e. U. ( R1 " On ) -> ( A e. A -> ( rank ` A ) e. ( rank ` A ) ) ) |
|
| 4 | 2 3 | mtoi | |- ( A e. U. ( R1 " On ) -> -. A e. A ) |