Theorem sosn

Description: Strict ordering on a singleton. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Assertion	sosn	$$⊢\mathrm{Rel}R\to \left(R\mathrm{Or}\left\{A\right\}\leftrightarrow \neg ARA\right)$$

Proof

Step	Hyp	Ref	Expression
1		elsni	$$⊢x\in \left\{A\right\}\to x=A$$
2		elsni	$$⊢y\in \left\{A\right\}\to y=A$$
3	2	eqcomd	$$⊢y\in \left\{A\right\}\to A=y$$
4	1 3	sylan9eq	$$⊢\left(x\in \left\{A\right\}\wedge y\in \left\{A\right\}\right)\to x=y$$
5	4	3mix2d	$$⊢\left(x\in \left\{A\right\}\wedge y\in \left\{A\right\}\right)\to \left(xRy\vee x=y\vee yRx\right)$$
6	5	rgen2	$$⊢\forall x\in \left\{A\right\}\forall y\in \left\{A\right\}\left(xRy\vee x=y\vee yRx\right)$$
7		df-so	$$⊢R\mathrm{Or}\left\{A\right\}\leftrightarrow \left(R\mathrm{Po}\left\{A\right\}\wedge \forall x\in \left\{A\right\}\forall y\in \left\{A\right\}\left(xRy\vee x=y\vee yRx\right)\right)$$
8	6 7	mpbiran2	$$⊢R\mathrm{Or}\left\{A\right\}\leftrightarrow R\mathrm{Po}\left\{A\right\}$$
9		posn	$$⊢\mathrm{Rel}R\to \left(R\mathrm{Po}\left\{A\right\}\leftrightarrow \neg ARA\right)$$
10	8 9	bitrid	$$⊢\mathrm{Rel}R\to \left(R\mathrm{Or}\left\{A\right\}\leftrightarrow \neg ARA\right)$$