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