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

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

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