Theorem sspsstri

Description: Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004)

	Ref	Expression
Assertion	sspsstri	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\leftrightarrow \left(A\subset B\vee A=B\vee B\subset A\right)$$

Proof

Step	Hyp	Ref	Expression
1		or32	$$⊢\left(\left(A\subset B\vee B\subset A\right)\vee A=B\right)\leftrightarrow \left(\left(A\subset B\vee A=B\right)\vee B\subset A\right)$$
2		sspss	$$⊢A\subseteq B\leftrightarrow \left(A\subset B\vee A=B\right)$$
3		sspss	$$⊢B\subseteq A\leftrightarrow \left(B\subset A\vee B=A\right)$$
4		eqcom	$$⊢B=A\leftrightarrow A=B$$
5	4	orbi2i	$$⊢\left(B\subset A\vee B=A\right)\leftrightarrow \left(B\subset A\vee A=B\right)$$
6	3 5	bitri	$$⊢B\subseteq A\leftrightarrow \left(B\subset A\vee A=B\right)$$
7	2 6	orbi12i	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\leftrightarrow \left(\left(A\subset B\vee A=B\right)\vee \left(B\subset A\vee A=B\right)\right)$$
8		orordir	$$⊢\left(\left(A\subset B\vee B\subset A\right)\vee A=B\right)\leftrightarrow \left(\left(A\subset B\vee A=B\right)\vee \left(B\subset A\vee A=B\right)\right)$$
9	7 8	bitr4i	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\leftrightarrow \left(\left(A\subset B\vee B\subset A\right)\vee A=B\right)$$
10		df-3or	$$⊢\left(A\subset B\vee A=B\vee B\subset A\right)\leftrightarrow \left(\left(A\subset B\vee A=B\right)\vee B\subset A\right)$$
11	1 9 10	3bitr4i	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\leftrightarrow \left(A\subset B\vee A=B\vee B\subset A\right)$$