This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. For a shorter proof requiring ax-un , see epweonALT . (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