Theorem wecmpep

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

	Ref	Expression
Assertion	wecmpep	$$⊢\left(\mathrm{E}\mathrm{We}A\wedge \left(x\in A\wedge y\in A\right)\right)\to \left(x\in y\vee x=y\vee y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		weso	$$⊢\mathrm{E}\mathrm{We}A\to \mathrm{E}\mathrm{Or}A$$
2		solin	$$⊢\left(\mathrm{E}\mathrm{Or}A\wedge \left(x\in A\wedge y\in A\right)\right)\to \left(x\mathrm{E}y\vee x=y\vee y\mathrm{E}x\right)$$
3		epel	$$⊢x\mathrm{E}y\leftrightarrow x\in y$$
4		biid	$$⊢x=y\leftrightarrow x=y$$
5		epel	$$⊢y\mathrm{E}x\leftrightarrow y\in x$$
6	3 4 5	3orbi123i	$$⊢\left(x\mathrm{E}y\vee x=y\vee y\mathrm{E}x\right)\leftrightarrow \left(x\in y\vee x=y\vee y\in x\right)$$
7	2 6	sylib	$$⊢\left(\mathrm{E}\mathrm{Or}A\wedge \left(x\in A\wedge y\in A\right)\right)\to \left(x\in y\vee x=y\vee y\in x\right)$$
8	1 7	sylan	$$⊢\left(\mathrm{E}\mathrm{We}A\wedge \left(x\in A\wedge y\in A\right)\right)\to \left(x\in y\vee x=y\vee y\in x\right)$$