Theorem smo0

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

	Ref	Expression
Assertion	smo0	$$⊢\mathrm{Smo}\varnothing$$

Proof

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