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	⊢ 𝑅 Po ∅

Proof

Step	Hyp	Ref	Expression
1		ral0	⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
2		df-po	⊢ ( 𝑅 Po ∅ ↔ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
3	1 2	mpbir	⊢ 𝑅 Po ∅