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

Metamath Proof Explorer

Theorem 0pos

Proof