Metamath Proof Explorer

Theorem wetrep

Description: On a class well-ordered by membership, the membership predicate is transitive. (Contributed by NM, 22-Apr-1994)

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

Proof

Step Hyp Ref Expression
1 weso 
 |-  ( _E We A -> _E Or A )
2 sotr 
 |-  ( ( _E Or A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x _E y /\ y _E z ) -> x _E z ) )
3 1 2 sylan 
 |-  ( ( _E We A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x _E y /\ y _E z ) -> x _E z ) )
4 epel 
 |-  ( x _E y <-> x e. y )
5 epel 
 |-  ( y _E z <-> y e. z )
6 4 5 anbi12i 
 |-  ( ( x _E y /\ y _E z ) <-> ( x e. y /\ y e. z ) )
7 epel 
 |-  ( x _E z <-> x e. z )
8 3 6 7 3imtr3g 
 |-  ( ( _E We A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x e. y /\ y e. z ) -> x e. z ) )