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 \land (x \in A \land y \in A \land z \in A)) \to ((x \in y \land y \in z) \to x \in z)$

Step	Hyp	Ref	Expression
1		weso	$⊢ E We A \to E Or A$
2		sotr	$⊢ (E Or A \land (x \in A \land y \in A \land z \in A)) \to ((x E y \land y E z) \to x E z)$
3	1 2	sylan	$⊢ (E We A \land (x \in A \land y \in A \land z \in A)) \to ((x E y \land y E z) \to x E z)$
4		epel	$⊢ x E y \leftrightarrow x \in y$
5		epel	$⊢ y E z \leftrightarrow y \in z$
6	4 5	anbi12i	$⊢ (x E y \land y E z) \leftrightarrow (x \in y \land y \in z)$
7		epel	$⊢ x E z \leftrightarrow x \in z$
8	3 6 7	3imtr3g	$⊢ (E We A \land (x \in A \land y \in A \land z \in A)) \to ((x \in y \land y \in z) \to x \in z)$

Metamath Proof Explorer