Theorem sorpss

Description: Express strict ordering under proper subsets, i.e. the notion of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Assertion	sorpss	$$⊢[\subset ]\mathrm{Or}A\leftrightarrow \forall x\in A\forall y\in A\left(x\subseteq y\vee y\subseteq x\right)$$

Proof

Step	Hyp	Ref	Expression
1		porpss	$$⊢[\subset ]\mathrm{Po}A$$
2	1	biantrur	$$⊢\forall x\in A\forall y\in A\left(x[\subset ]y\vee x=y\vee y[\subset ]x\right)\leftrightarrow \left([\subset ]\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(x[\subset ]y\vee x=y\vee y[\subset ]x\right)\right)$$
3		sspsstri	$$⊢\left(x\subseteq y\vee y\subseteq x\right)\leftrightarrow \left(x\subset y\vee x=y\vee y\subset x\right)$$
4		vex	$$⊢y\in \mathrm{V}$$
5	4	brrpss	$$⊢x[\subset ]y\leftrightarrow x\subset y$$
6		biid	$$⊢x=y\leftrightarrow x=y$$
7		vex	$$⊢x\in \mathrm{V}$$
8	7	brrpss	$$⊢y[\subset ]x\leftrightarrow y\subset x$$
9	5 6 8	3orbi123i	$$⊢\left(x[\subset ]y\vee x=y\vee y[\subset ]x\right)\leftrightarrow \left(x\subset y\vee x=y\vee y\subset x\right)$$
10	3 9	bitr4i	$$⊢\left(x\subseteq y\vee y\subseteq x\right)\leftrightarrow \left(x[\subset ]y\vee x=y\vee y[\subset ]x\right)$$
11	10	2ralbii	$$⊢\forall x\in A\forall y\in A\left(x\subseteq y\vee y\subseteq x\right)\leftrightarrow \forall x\in A\forall y\in A\left(x[\subset ]y\vee x=y\vee y[\subset ]x\right)$$
12		df-so	$$⊢[\subset ]\mathrm{Or}A\leftrightarrow \left([\subset ]\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(x[\subset ]y\vee x=y\vee y[\subset ]x\right)\right)$$
13	2 11 12	3bitr4ri	$$⊢[\subset ]\mathrm{Or}A\leftrightarrow \forall x\in A\forall y\in A\left(x\subseteq y\vee y\subseteq x\right)$$