Metamath Proof Explorer

Theorem so0

Description: Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion so0 
|- R Or (/)

Proof

Step Hyp Ref Expression
1 po0 
 |-  R Po (/)
2 ral0 
 |-  A. x e. (/) A. y e. (/) ( x R y \/ x = y \/ y R x )
3 df-so 
 |-  ( R Or (/) <-> ( R Po (/) /\ A. x e. (/) A. y e. (/) ( x R y \/ x = y \/ y R x ) ) )
4 1 2 3 mpbir2an 
 |-  R Or (/)