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	⊢ ∀ 𝑎 ∈ ∅ ∀ 𝑏 ∈ ∅ ∀ 𝑐 ∈ ∅ ( 𝑎 ∅ 𝑎 ∧ ( ( 𝑎 ∅ 𝑏 ∧ 𝑏 ∅ 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ∅ 𝑏 ∧ 𝑏 ∅ 𝑐 ) → 𝑎 ∅ 𝑐 ) )
3		base0	⊢ ∅ = ( Base ‘ ∅ )
4		df-ple	⊢ le = Slot ; 1 0
5	4	str0	⊢ ∅ = ( le ‘ ∅ )
6	3 5	ispos	⊢ ( ∅ ∈ Poset ↔ ( ∅ ∈ V ∧ ∀ 𝑎 ∈ ∅ ∀ 𝑏 ∈ ∅ ∀ 𝑐 ∈ ∅ ( 𝑎 ∅ 𝑎 ∧ ( ( 𝑎 ∅ 𝑏 ∧ 𝑏 ∅ 𝑎 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑎 ∅ 𝑏 ∧ 𝑏 ∅ 𝑐 ) → 𝑎 ∅ 𝑐 ) ) ) )
7	1 2 6	mpbir2an	⊢ ∅ ∈ Poset