Theorem so0

Description: Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	so0	⊢ 𝑅 Or ∅

Proof

Step	Hyp	Ref	Expression
1		po0	⊢ 𝑅 Po ∅
2		ral0	⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 )
3		df-so	⊢ ( 𝑅 Or ∅ ↔ ( 𝑅 Po ∅ ∧ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
4	1 2 3	mpbir2an	⊢ 𝑅 Or ∅