This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )