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 \emptyset$

Step	Hyp	Ref	Expression
1		ral0	$⊢ \forall x \in \emptyset \forall y \in \emptyset \forall z \in \emptyset (\neg x R x \land ((x R y \land y R z) \to x R z))$
2		df-po	$⊢ R Po \emptyset \leftrightarrow \forall x \in \emptyset \forall y \in \emptyset \forall z \in \emptyset (\neg x R x \land ((x R y \land y R z) \to x R z))$
3	1 2	mpbir	$⊢ R Po \emptyset$