This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordge1n0

Description: An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004)

		Ref	Expression
	Assertion	ordge1n0	$⊢ Ord A \to (1_{𝑜} \subseteq A \leftrightarrow A \neq \emptyset)$

Step	Hyp	Ref	Expression
1		ordgt0ge1	$⊢ Ord A \to (\emptyset \in A \leftrightarrow 1_{𝑜} \subseteq A)$
2		ord0eln0	$⊢ Ord A \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
3	1 2	bitr3d	$⊢ Ord A \to (1_{𝑜} \subseteq A \leftrightarrow A \neq \emptyset)$