Metamath Proof Explorer

Theorem 0pos

Description: Technical lemma to simplify the statement of ipopos . The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set ( str0 ) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015) (Proof shortened by AV, 13-Oct-2024)

Ref Expression
Assertion 0pos ⊢ ∅ ∈ Poset

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 ral0 ⊢ ∀ a ∈ ∅ ∀ b ∈ ∅ ∀ c ∈ ∅ a ∅ a ∧ a ∅ b ∧ b ∅ a → a = b ∧ a ∅ b ∧ b ∅ c → a ∅ c
3 base0 ⊢ ∅ = Base ∅
4 pleid ⊢ le = Slot ≤ ndx
5 4 str0 ⊢ ∅ = ≤ ∅
6 3 5 ispos ⊢ ∅ ∈ Poset ↔ ∅ ∈ V ∧ ∀ a ∈ ∅ ∀ b ∈ ∅ ∀ c ∈ ∅ a ∅ a ∧ a ∅ b ∧ b ∅ a → a = b ∧ a ∅ b ∧ b ∅ c → a ∅ c
7 1 2 6 mpbir2an ⊢ ∅ ∈ Poset