Metamath Proof Explorer

Theorem 0posOLD

Description: Obsolete proof of 0pos as of 13-Oct-2024. (Contributed by Stefan O'Rear, 30-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 0posOLD ⊢ ∅ ∈ 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 df-ple ⊢ le = Slot 10
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