Metamath Proof Explorer

Theorem po0

Description: Any relation is a partial order on the empty set. (Contributed by NM, 28-Mar-1997) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion po0 
|- R Po (/)

Proof

Step Hyp Ref Expression
1 ral0 
 |-  A. x e. (/) A. y e. (/) A. z e. (/) ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
2 df-po 
 |-  ( R Po (/) <-> A. x e. (/) A. y e. (/) A. z e. (/) ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
3 1 2 mpbir 
 |-  R Po (/)