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 ⊢ ∀ x ∈ ∅ ∀ y ∈ ∅ ∀ z ∈ ∅ ¬ x R x ∧ x R y ∧ y R z → x R z
2 df-po ⊢ R Po ∅ ↔ ∀ x ∈ ∅ ∀ y ∈ ∅ ∀ z ∈ ∅ ¬ x R x ∧ x R y ∧ y R z → x R z
3 1 2 mpbir ⊢ R Po ∅