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

Metamath Proof Explorer

Theorem epweonALT

Description: Alternate proof of epweon , shorter but requiring ax-un . (Contributed by NM, 1-Nov-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion epweonALT 
|- _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