Metamath Proof Explorer


Theorem wfelirr

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 )

Proof

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 )