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

Metamath Proof Explorer

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 ∅