Theorem epweon

Description: The membership relation well-orders the class of ordinal numbers. This proof does not require the axiom of regularity. Proposition 4.8(g) of Mendelson p. 244. (Contributed by NM, 1-Nov-2003)

	Ref	Expression
Assertion	epweon	|- _E We On

Proof

Step	Hyp	Ref	Expression
1		onfr	|- _E Fr On
2		eloni	|- ( x e. On -> Ord x )
3		eloni	|- ( y e. On -> Ord y )
4		ordtri3or	|- ( ( Ord x /\ Ord y ) -> ( x e. y \/ x = y \/ y e. x ) )
5		epel	|- ( x _E y <-> x e. y )
6		biid	|- ( x = y <-> x = y )
7		epel	|- ( y _E x <-> y e. x )
8	5 6 7	3orbi123i	|- ( ( x _E y \/ x = y \/ y _E x ) <-> ( x e. y \/ x = y \/ y e. x ) )
9	4 8	sylibr	|- ( ( Ord x /\ Ord y ) -> ( x _E y \/ x = y \/ y _E x ) )
10	2 3 9	syl2an	|- ( ( x e. On /\ y e. On ) -> ( x _E y \/ x = y \/ y _E x ) )
11	10	rgen2	|- A. x e. On A. y e. On ( x _E y \/ x = y \/ y _E x )
12		dfwe2	|- ( _E We On <-> ( _E Fr On /\ A. x e. On A. y e. On ( x _E y \/ x = y \/ y _E x ) ) )
13	1 11 12	mpbir2an	|- _E We On