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	$⊢ \emptyset \in Poset$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		ral0	$⊢ \forall a \in \emptyset \forall b \in \emptyset \forall c \in \emptyset (a \emptyset a \land ((a \emptyset b \land b \emptyset a) \to a = b) \land ((a \emptyset b \land b \emptyset c) \to a \emptyset c))$
3		base0	$⊢ \emptyset = {Base}_{\emptyset}$
4		pleid	$⊢ le = Slot \leq_{ndx}$
5	4	str0	$⊢ \emptyset = \leq_{\emptyset}$
6	3 5	ispos	$⊢ \emptyset \in Poset \leftrightarrow (\emptyset \in V \land \forall a \in \emptyset \forall b \in \emptyset \forall c \in \emptyset (a \emptyset a \land ((a \emptyset b \land b \emptyset a) \to a = b) \land ((a \emptyset b \land b \emptyset c) \to a \emptyset c)))$
7	1 2 6	mpbir2an	$⊢ \emptyset \in Poset$

Metamath Proof Explorer

Theorem 0pos

Proof