Metamath Proof Explorer

Theorem wecmpep

Description: The elements of a class well-ordered by membership are comparable. (Contributed by NM, 17-May-1994)

Ref Expression
Assertion wecmpep 
|- ( ( _E We A /\ ( x e. A /\ y e. A ) ) -> ( x e. y \/ x = y \/ y e. x ) )

Proof

Step Hyp Ref Expression
1 weso 
 |-  ( _E We A -> _E Or A )
2 solin 
 |-  ( ( _E Or A /\ ( x e. A /\ y e. A ) ) -> ( x _E y \/ x = y \/ y _E x ) )
3 epel 
 |-  ( x _E y <-> x e. y )
4 biid 
 |-  ( x = y <-> x = y )
5 epel 
 |-  ( y _E x <-> y e. x )
6 3 4 5 3orbi123i 
 |-  ( ( x _E y \/ x = y \/ y _E x ) <-> ( x e. y \/ x = y \/ y e. x ) )
7 2 6 sylib 
 |-  ( ( _E Or A /\ ( x e. A /\ y e. A ) ) -> ( x e. y \/ x = y \/ y e. x ) )
8 1 7 sylan 
 |-  ( ( _E We A /\ ( x e. A /\ y e. A ) ) -> ( x e. y \/ x = y \/ y e. x ) )