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

Step	Hyp	Ref	Expression
1		weso	$⊢ E We A \to E Or A$
2		solin	$⊢ (E Or A \land (x \in A \land y \in A)) \to (x E y \lor x = y \lor y E x)$
3		epel	$⊢ x E y \leftrightarrow x \in y$
4		biid	$⊢ x = y \leftrightarrow x = y$
5		epel	$⊢ y E x \leftrightarrow y \in x$
6	3 4 5	3orbi123i	$⊢ (x E y \lor x = y \lor y E x) \leftrightarrow (x \in y \lor x = y \lor y \in x)$
7	2 6	sylib	$⊢ (E Or A \land (x \in A \land y \in A)) \to (x \in y \lor x = y \lor y \in x)$
8	1 7	sylan	$⊢ (E We A \land (x \in A \land y \in A)) \to (x \in y \lor x = y \lor y \in x)$

Metamath Proof Explorer