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) Avoid ax-un . (Revised by BTernaryTau, 30-Nov-2024)

	Ref	Expression
Assertion	epweon	|- _E We On

Proof

Step	Hyp	Ref	Expression
1		onfr	|- _E Fr On
2		df-po	|- ( _E Po On <-> A. x e. On A. y e. On A. z e. On ( -. x _E x /\ ( ( x _E y /\ y _E z ) -> x _E z ) ) )
3		eloni	|- ( x e. On -> Ord x )
4		ordirr	|- ( Ord x -> -. x e. x )
5	3 4	syl	|- ( x e. On -> -. x e. x )
6		epel	|- ( x _E x <-> x e. x )
7	5 6	sylnibr	|- ( x e. On -> -. x _E x )
8		ontr1	|- ( z e. On -> ( ( x e. y /\ y e. z ) -> x e. z ) )
9		epel	|- ( x _E y <-> x e. y )
10		epel	|- ( y _E z <-> y e. z )
11	9 10	anbi12i	|- ( ( x _E y /\ y _E z ) <-> ( x e. y /\ y e. z ) )
12		epel	|- ( x _E z <-> x e. z )
13	8 11 12	3imtr4g	|- ( z e. On -> ( ( x _E y /\ y _E z ) -> x _E z ) )
14	7 13	anim12i	|- ( ( x e. On /\ z e. On ) -> ( -. x _E x /\ ( ( x _E y /\ y _E z ) -> x _E z ) ) )
15	14	ralrimiva	|- ( x e. On -> A. z e. On ( -. x _E x /\ ( ( x _E y /\ y _E z ) -> x _E z ) ) )
16	15	ralrimivw	|- ( x e. On -> A. y e. On A. z e. On ( -. x _E x /\ ( ( x _E y /\ y _E z ) -> x _E z ) ) )
17	2 16	mprgbir	|- _E Po On
18		eloni	|- ( y e. On -> Ord y )
19		ordtri3or	|- ( ( Ord x /\ Ord y ) -> ( x e. y \/ x = y \/ y e. x ) )
20		biid	|- ( x = y <-> x = y )
21		epel	|- ( y _E x <-> y e. x )
22	9 20 21	3orbi123i	|- ( ( x _E y \/ x = y \/ y _E x ) <-> ( x e. y \/ x = y \/ y e. x ) )
23	19 22	sylibr	|- ( ( Ord x /\ Ord y ) -> ( x _E y \/ x = y \/ y _E x ) )
24	3 18 23	syl2an	|- ( ( x e. On /\ y e. On ) -> ( x _E y \/ x = y \/ y _E x ) )
25	24	rgen2	|- A. x e. On A. y e. On ( x _E y \/ x = y \/ y _E x )
26		df-so	|- ( _E Or On <-> ( _E Po On /\ A. x e. On A. y e. On ( x _E y \/ x = y \/ y _E x ) ) )
27	17 25 26	mpbir2an	|- _E Or On
28		df-we	|- ( _E We On <-> ( _E Fr On /\ _E Or On ) )
29	1 27 28	mpbir2an	|- _E We On