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

Metamath Proof Explorer

Theorem smo0

Description: The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011)

		Ref	Expression
	Assertion	smo0	$⊢ Smo \emptyset$

Step	Hyp	Ref	Expression
1		ord0	$⊢ Ord \emptyset$
2	1	iordsmo	$⊢ Smo ({I ↾}_{\emptyset})$
3		res0	$⊢ {I ↾}_{\emptyset} = \emptyset$
4		smoeq	$⊢ {I ↾}_{\emptyset} = \emptyset \to (Smo ({I ↾}_{\emptyset}) \leftrightarrow Smo \emptyset)$
5	3 4	ax-mp	$⊢ Smo ({I ↾}_{\emptyset}) \leftrightarrow Smo \emptyset$
6	2 5	mpbi	$⊢ Smo \emptyset$