Theorem sosn

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

	Ref	Expression
Assertion	sosn	|- ( Rel R -> ( R Or { A } <-> -. A R A ) )

Proof

Step	Hyp	Ref	Expression
1		elsni	|- ( x e. { A } -> x = A )
2		elsni	|- ( y e. { A } -> y = A )
3	2	eqcomd	|- ( y e. { A } -> A = y )
4	1 3	sylan9eq	|- ( ( x e. { A } /\ y e. { A } ) -> x = y )
5	4	3mix2d	|- ( ( x e. { A } /\ y e. { A } ) -> ( x R y \/ x = y \/ y R x ) )
6	5	rgen2	|- A. x e. { A } A. y e. { A } ( x R y \/ x = y \/ y R x )
7		df-so	|- ( R Or { A } <-> ( R Po { A } /\ A. x e. { A } A. y e. { A } ( x R y \/ x = y \/ y R x ) ) )
8	6 7	mpbiran2	|- ( R Or { A } <-> R Po { A } )
9		posn	|- ( Rel R -> ( R Po { A } <-> -. A R A ) )
10	8 9	bitrid	|- ( Rel R -> ( R Or { A } <-> -. A R A ) )